type name;
type ref;
const unique null : ref;
type real;
type elements;
type struct;
type exposeVersionType;
var $Heap : <x>[ref, name]x where IsHeap($Heap);
function IsHeap(h : <x>[ref, name]x) returns ($$unnamed~a : bool);
const $allocated : name;
const $elements : name;
const $inv : name;
const $localinv : name;
const $exposeVersion : name;
axiom (DeclType($exposeVersion) == System.Object);
const $sharingMode : name;
const $SharingMode_Unshared : name;
const $SharingMode_LockProtected : name;
const $ownerRef : name;
const $ownerFrame : name;
const $PeerGroupPlaceholder : name;
function ClassRepr(class : name) returns ($$unnamed~b : ref);
axiom (forall c0 : name, c1 : name :: {ClassRepr(c0), ClassRepr(c1)} ((c0 != c1) ==> (ClassRepr(c0) != ClassRepr(c1))));
axiom (forall T : name :: !($typeof(ClassRepr(T)) <: System.Object));
axiom (forall T : name :: (ClassRepr(T) != null));
axiom (forall T : name, h : <x>[ref, name]x :: {h[ClassRepr(T), $ownerFrame]} (IsHeap(h) ==> (h[ClassRepr(T), $ownerFrame] == $PeerGroupPlaceholder)));
function IsDirectlyModifiableField(f : name) returns ($$unnamed~c : bool);
axiom !IsDirectlyModifiableField($allocated);
axiom IsDirectlyModifiableField($elements);
axiom !IsDirectlyModifiableField($inv);
axiom !IsDirectlyModifiableField($localinv);
axiom !IsDirectlyModifiableField($ownerRef);
axiom !IsDirectlyModifiableField($ownerFrame);
axiom !IsDirectlyModifiableField($exposeVersion);
function IsStaticField(f : name) returns ($$unnamed~d : bool);
axiom !IsStaticField($allocated);
axiom !IsStaticField($elements);
axiom !IsStaticField($inv);
axiom !IsStaticField($localinv);
axiom !IsStaticField($exposeVersion);
function ValueArrayGet<any>($$unnamed~f : elements, $$unnamed~e : int) returns ($$unnamed~g : any);
function ValueArraySet<any>($$unnamed~j : elements, $$unnamed~i : int, $$unnamed~h : any) returns ($$unnamed~k : elements);
function RefArrayGet($$unnamed~m : elements, $$unnamed~l : int) returns ($$unnamed~n : ref);
function RefArraySet($$unnamed~q : elements, $$unnamed~p : int, $$unnamed~o : ref) returns ($$unnamed~r : elements);
axiom (forall<any> A : elements, i : int, x : any :: (ValueArrayGet(ValueArraySet(A, i, x), i) == x));
axiom (forall<any> A : elements, i : int, j : int, x : any :: ((i != j) ==> (ValueArrayGet(ValueArraySet(A, i, x), j) == ValueArrayGet(A, j))));
axiom (forall A : elements, i : int, x : ref :: (RefArrayGet(RefArraySet(A, i, x), i) == x));
axiom (forall A : elements, i : int, j : int, x : ref :: ((i != j) ==> (RefArrayGet(RefArraySet(A, i, x), j) == RefArrayGet(A, j))));
function ArrayIndex(arr : ref, dim : int, indexAtDim : int, remainingIndexContribution : int) returns ($$unnamed~s : int);
axiom (forall a : ref, d : int, x : int, y : int, x' : int, y' : int :: {ArrayIndex(a, d, x, y), ArrayIndex(a, d, x', y')} ((ArrayIndex(a, d, x, y) == ArrayIndex(a, d, x', y')) ==> ((x == x') && (y == y'))));
axiom (forall a : ref, T : name, i : int, r : int, heap : <x>[ref, name]x :: {($typeof(a) <: RefArray(T, r)), RefArrayGet(heap[a, $elements], i)} ((IsHeap(heap) && ($typeof(a) <: RefArray(T, r))) ==> $Is(RefArrayGet(heap[a, $elements], i), T)));
axiom (forall a : ref, T : name, i : int, r : int, heap : <x>[ref, name]x :: {($typeof(a) <: NonNullRefArray(T, r)), RefArrayGet(heap[a, $elements], i)} ((IsHeap(heap) && ($typeof(a) <: NonNullRefArray(T, r))) ==> $IsNotNull(RefArrayGet(heap[a, $elements], i), T)));
function $Rank($$unnamed~t : ref) returns ($$unnamed~u : int);
axiom (forall a : ref :: (1 <= $Rank(a)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: RefArray(T, r))} (((a != null) && ($typeof(a) <: RefArray(T, r))) ==> ($Rank(a) == r)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: NonNullRefArray(T, r))} (((a != null) && ($typeof(a) <: NonNullRefArray(T, r))) ==> ($Rank(a) == r)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: ValueArray(T, r))} (((a != null) && ($typeof(a) <: ValueArray(T, r))) ==> ($Rank(a) == r)));
function $Length($$unnamed~v : ref) returns ($$unnamed~w : int);
axiom (forall a : ref :: {$Length(a)} (0 <= $Length(a)));
function $DimLength($$unnamed~y : ref, $$unnamed~x : int) returns ($$unnamed~z : int);
axiom (forall a : ref, i : int :: (0 <= $DimLength(a, i)));
axiom (forall a : ref :: {$DimLength(a, 0)} (($Rank(a) == 1) ==> ($DimLength(a, 0) == $Length(a))));
function $LBound($$unnamed~ab : ref, $$unnamed~aa : int) returns ($$unnamed~ac : int);
function $UBound($$unnamed~ae : ref, $$unnamed~ad : int) returns ($$unnamed~af : int);
axiom (forall a : ref, i : int :: {$LBound(a, i)} ($LBound(a, i) == 0));
axiom (forall a : ref, i : int :: {$UBound(a, i)} ($UBound(a, i) == ($DimLength(a, i) - 1)));
const $ArrayCategoryValue : name;
const $ArrayCategoryRef : name;
const $ArrayCategoryNonNullRef : name;
function $ArrayCategory(arrayType : name) returns (arrayCategory : name);
axiom (forall T : name, ET : name, r : int :: {(T <: ValueArray(ET, r))} ((T <: ValueArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryValue)));
axiom (forall T : name, ET : name, r : int :: {(T <: RefArray(ET, r))} ((T <: RefArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryRef)));
axiom (forall T : name, ET : name, r : int :: {(T <: NonNullRefArray(ET, r))} ((T <: NonNullRefArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryNonNullRef)));
const System.Array : name;
axiom (System.Array <: System.Object);
function $ElementType($$unnamed~ag : name) returns ($$unnamed~ah : name);
function ValueArray(elementType : name, rank : int) returns ($$unnamed~ai : name);
axiom (forall T : name, r : int :: {ValueArray(T, r)} (ValueArray(T, r) <: System.Array));
function RefArray(elementType : name, rank : int) returns ($$unnamed~aj : name);
axiom (forall T : name, r : int :: {RefArray(T, r)} (RefArray(T, r) <: System.Array));
function NonNullRefArray(elementType : name, rank : int) returns ($$unnamed~ak : name);
axiom (forall T : name, r : int :: {NonNullRefArray(T, r)} (NonNullRefArray(T, r) <: System.Array));
axiom (forall T : name, U : name, r : int :: ((U <: T) ==> (RefArray(U, r) <: RefArray(T, r))));
axiom (forall T : name, U : name, r : int :: ((U <: T) ==> (NonNullRefArray(U, r) <: NonNullRefArray(T, r))));
axiom (forall A : name, r : int :: ($ElementType(ValueArray(A, r)) == A));
axiom (forall A : name, r : int :: ($ElementType(RefArray(A, r)) == A));
axiom (forall A : name, r : int :: ($ElementType(NonNullRefArray(A, r)) == A));
axiom (forall A : name, r : int, T : name :: {(T <: RefArray(A, r))} ((T <: RefArray(A, r)) ==> ((T == RefArray($ElementType(T), r)) && ($ElementType(T) <: A))));
axiom (forall A : name, r : int, T : name :: {(T <: NonNullRefArray(A, r))} ((T <: NonNullRefArray(A, r)) ==> ((T == NonNullRefArray($ElementType(T), r)) && ($ElementType(T) <: A))));
axiom (forall A : name, r : int, T : name :: {(T <: ValueArray(A, r))} ((T <: ValueArray(A, r)) ==> (T == ValueArray(A, r))));
axiom (forall A : name, r : int, T : name :: ((RefArray(A, r) <: T) ==> ((System.Array <: T) || ((T == RefArray($ElementType(T), r)) && (A <: $ElementType(T))))));
axiom (forall A : name, r : int, T : name :: ((NonNullRefArray(A, r) <: T) ==> ((System.Array <: T) || ((T == NonNullRefArray($ElementType(T), r)) && (A <: $ElementType(T))))));
axiom (forall A : name, r : int, T : name :: ((ValueArray(A, r) <: T) ==> ((System.Array <: T) || (T == ValueArray(A, r)))));
function $ArrayPtr(elementType : name) returns ($$unnamed~al : name);
function $StructGet<any>($$unnamed~an : struct, $$unnamed~am : name) returns ($$unnamed~ao : any);
function $StructSet<any>($$unnamed~ar : struct, $$unnamed~aq : name, $$unnamed~ap : any) returns ($$unnamed~as : struct);
axiom (forall<any> s : struct, f : name, x : any :: ($StructGet($StructSet(s, f, x), f) == x));
axiom (forall<any> s : struct, f : name, f' : name, x : any :: ((f != f') ==> ($StructGet($StructSet(s, f, x), f') == $StructGet(s, f'))));
function ZeroInit(s : struct, typ : name) returns ($$unnamed~at : bool);
function $typeof($$unnamed~au : ref) returns ($$unnamed~av : name);
function $BaseClass(sub : name) returns (base : name);
function AsDirectSubClass(sub : name, base : name) returns (sub' : name);
function OneClassDown(sub : name, base : name) returns (directSub : name);
axiom (forall A : name, B : name, C : name :: {(C <: AsDirectSubClass(B, A))} ((C <: AsDirectSubClass(B, A)) ==> (OneClassDown(C, A) == B)));
function $IsValueType($$unnamed~aw : name) returns ($$unnamed~ax : bool);
axiom (forall T : name :: ($IsValueType(T) ==> ((forall U : name :: ((T <: U) ==> (T == U))) && (forall U : name :: ((U <: T) ==> (T == U))))));
const System.Object : name;
function $IsTokenForType($$unnamed~az : struct, $$unnamed~ay : name) returns ($$unnamed~ba : bool);
function TypeObject($$unnamed~bb : name) returns ($$unnamed~bc : ref);
const System.Type : name;
axiom (System.Type <: System.Object);
axiom (forall T : name :: {TypeObject(T)} $IsNotNull(TypeObject(T), System.Type));
function TypeName($$unnamed~bd : ref) returns ($$unnamed~be : name);
axiom (forall T : name :: {TypeObject(T)} (TypeName(TypeObject(T)) == T));
function $Is($$unnamed~bg : ref, $$unnamed~bf : name) returns ($$unnamed~bh : bool);
axiom (forall o : ref, T : name :: {$Is(o, T)} ($Is(o, T) <==> ((o == null) || ($typeof(o) <: T))));
function $IsNotNull($$unnamed~bj : ref, $$unnamed~bi : name) returns ($$unnamed~bk : bool);
axiom (forall o : ref, T : name :: {$IsNotNull(o, T)} ($IsNotNull(o, T) <==> ((o != null) && $Is(o, T))));
function $As($$unnamed~bm : ref, $$unnamed~bl : name) returns ($$unnamed~bn : ref);
axiom (forall o : ref, T : name :: ($Is(o, T) ==> ($As(o, T) == o)));
axiom (forall o : ref, T : name :: (!$Is(o, T) ==> ($As(o, T) == null)));
axiom (forall h : <x>[ref, name]x, o : ref :: {($typeof(o) <: System.Array), h[o, $inv]} (((IsHeap(h) && (o != null)) && ($typeof(o) <: System.Array)) ==> ((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o)))));
function IsAllocated<any>(h : <x>[ref, name]x, o : any) returns ($$unnamed~bo : bool);
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {IsAllocated(h, h[o, f])} ((IsHeap(h) && h[o, $allocated]) ==> IsAllocated(h, h[o, f])));
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {h[h[o, f], $allocated]} ((IsHeap(h) && h[o, $allocated]) ==> h[h[o, f], $allocated]));
axiom (forall h : <x>[ref, name]x, s : struct, f : name :: {IsAllocated(h, $StructGet(s, f))} (IsAllocated(h, s) ==> IsAllocated(h, $StructGet(s, f))));
axiom (forall h : <x>[ref, name]x, e : elements, i : int :: {IsAllocated(h, RefArrayGet(e, i))} (IsAllocated(h, e) ==> IsAllocated(h, RefArrayGet(e, i))));
axiom (forall h : <x>[ref, name]x, e : elements, i : int :: {IsAllocated(h, ValueArrayGet(e, i))} (IsAllocated(h, e) ==> IsAllocated(h, ValueArrayGet(e, i))));
axiom (forall h : <x>[ref, name]x, o : ref :: {h[o, $allocated]} (IsAllocated(h, o) ==> h[o, $allocated]));
axiom (forall h : <x>[ref, name]x, c : name :: {h[ClassRepr(c), $allocated]} (IsHeap(h) ==> h[ClassRepr(c), $allocated]));
const $BeingConstructed : ref;
const $NonNullFieldsAreInitialized : name;
function DeclType(field : name) returns (class : name);
function AsNonNullRefField(field : name, T : name) returns (f : name);
function AsRefField(field : name, T : name) returns (f : name);
function AsRangeField(field : name, T : name) returns (f : name);
axiom (forall f : name, T : name :: {AsNonNullRefField(f, T)} ((AsNonNullRefField(f, T) == f) ==> (AsRefField(f, T) == f)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRefField(f, T)]} (IsHeap(h) ==> $Is(h[o, AsRefField(f, T)], T)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsNonNullRefField(f, T)]} (((IsHeap(h) && (o != null)) && ((o != $BeingConstructed) || (h[$BeingConstructed, $NonNullFieldsAreInitialized] == true))) ==> (h[o, AsNonNullRefField(f, T)] != null)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRangeField(f, T)]} (IsHeap(h) ==> InRange(h[o, AsRangeField(f, T)], T)));
function $IsMemberlessType($$unnamed~bp : name) returns ($$unnamed~bq : bool);
axiom (forall o : ref :: {$IsMemberlessType($typeof(o))} !$IsMemberlessType($typeof(o)));
function $IsImmutable(T : name) returns ($$unnamed~br : bool);
axiom !$IsImmutable(System.Object);
function $AsImmutable(T : name) returns (theType : name);
function $AsMutable(T : name) returns (theType : name);
axiom (forall T : name, U : name :: {(U <: $AsImmutable(T))} ((U <: $AsImmutable(T)) ==> ($IsImmutable(U) && ($AsImmutable(U) == U))));
axiom (forall T : name, U : name :: {(U <: $AsMutable(T))} ((U <: $AsMutable(T)) ==> (!$IsImmutable(U) && ($AsMutable(U) == U))));
function AsOwner(string : ref, owner : ref) returns (theString : ref);
axiom (forall o : ref, T : name :: {($typeof(o) <: $AsImmutable(T))} ((((o != null) && (o != $BeingConstructed)) && ($typeof(o) <: $AsImmutable(T))) ==> (forall h : <x>[ref, name]x :: {IsHeap(h)} (IsHeap(h) ==> (((((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o))) && (h[o, $ownerFrame] == $PeerGroupPlaceholder)) && (AsOwner(o, h[o, $ownerRef]) == o)) && (forall t : ref :: {AsOwner(o, h[t, $ownerRef])} ((AsOwner(o, h[t, $ownerRef]) == o) ==> ((t == o) || (h[t, $ownerFrame] != $PeerGroupPlaceholder)))))))));
const System.String : name;
function $StringLength($$unnamed~bs : ref) returns ($$unnamed~bt : int);
axiom (forall s : ref :: {$StringLength(s)} (0 <= $StringLength(s)));
function AsRepField(f : name, declaringType : name) returns (theField : name);
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRepField(f, T)]} ((IsHeap(h) && (h[o, AsRepField(f, T)] != null)) ==> ((h[h[o, AsRepField(f, T)], $ownerRef] == o) && (h[h[o, AsRepField(f, T)], $ownerFrame] == T))));
function AsPeerField(f : name) returns (theField : name);
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {h[o, AsPeerField(f)]} ((IsHeap(h) && (h[o, AsPeerField(f)] != null)) ==> ((h[h[o, AsPeerField(f)], $ownerRef] == h[o, $ownerRef]) && (h[h[o, AsPeerField(f)], $ownerFrame] == h[o, $ownerFrame]))));
axiom (forall h : <x>[ref, name]x, o : ref :: {(h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])} ((((IsHeap(h) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> ((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o)))));
procedure $SetOwner(o : ref, ow : ref, fr : name);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} (((((F != $ownerRef) && (F != $ownerFrame)) || old(($Heap[p, $ownerRef] != $Heap[o, $ownerRef]))) || old(($Heap[p, $ownerFrame] != $Heap[o, $ownerFrame]))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} ((old(($Heap[p, $ownerRef] == $Heap[o, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[o, $ownerFrame]))) ==> (($Heap[p, $ownerRef] == ow) && ($Heap[p, $ownerFrame] == fr))));
  

procedure $UpdateOwnersForRep(o : ref, T : name, e : ref);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} (((((F != $ownerRef) && (F != $ownerFrame)) || old(($Heap[p, $ownerRef] != $Heap[e, $ownerRef]))) || old(($Heap[p, $ownerFrame] != $Heap[e, $ownerFrame]))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures ((e == null) ==> ($Heap == old($Heap)));
  ensures ((e != null) ==> (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} ((old(($Heap[p, $ownerRef] == $Heap[e, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[e, $ownerFrame]))) ==> (($Heap[p, $ownerRef] == o) && ($Heap[p, $ownerFrame] == T)))));
  

procedure $UpdateOwnersForPeer(c : ref, d : ref);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} ((((F != $ownerRef) && (F != $ownerFrame)) || old(((($Heap[p, $ownerRef] != $Heap[c, $ownerRef]) || ($Heap[p, $ownerFrame] != $Heap[c, $ownerFrame])) && (($Heap[p, $ownerRef] != $Heap[d, $ownerRef]) || ($Heap[p, $ownerFrame] != $Heap[d, $ownerFrame]))))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures ((d == null) ==> ($Heap == old($Heap)));
  ensures ((d != null) ==> (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} (((old(($Heap[p, $ownerRef] == $Heap[c, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[c, $ownerFrame]))) || (old(($Heap[p, $ownerRef] == $Heap[d, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[d, $ownerFrame])))) ==> ((((old($Heap)[d, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[p, $ownerRef] == old($Heap)[c, $ownerRef])) && ($Heap[p, $ownerFrame] == old($Heap)[c, $ownerFrame])) || (((old($Heap)[d, $ownerFrame] != $PeerGroupPlaceholder) && ($Heap[p, $ownerRef] == old($Heap)[d, $ownerRef])) && ($Heap[p, $ownerFrame] == old($Heap)[d, $ownerFrame]))))));
  

const $FirstConsistentOwner : name;
function $AsPureObject($$unnamed~bu : ref) returns ($$unnamed~bv : ref);
function ##FieldDependsOnFCO<any>(o : ref, f : name, ev : exposeVersionType) returns (value : any);
axiom (forall o : ref, f : name, h : <x>[ref, name]x :: {h[$AsPureObject(o), f]} ((((((IsHeap(h) && (o != null)) && (h[o, $allocated] == true)) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> (h[o, f] == ##FieldDependsOnFCO(o, f, h[h[o, $FirstConsistentOwner], $exposeVersion]))));
axiom (forall o : ref, h : <x>[ref, name]x :: {h[o, $FirstConsistentOwner]} ((((((IsHeap(h) && (o != null)) && (h[o, $allocated] == true)) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> (((h[o, $FirstConsistentOwner] != null) && (h[h[o, $FirstConsistentOwner], $allocated] == true)) && (((h[h[o, $FirstConsistentOwner], $ownerFrame] == $PeerGroupPlaceholder) || !(h[h[h[o, $FirstConsistentOwner], $ownerRef], $inv] <: h[h[o, $FirstConsistentOwner], $ownerFrame])) || (h[h[h[o, $FirstConsistentOwner], $ownerRef], $localinv] == $BaseClass(h[h[o, $FirstConsistentOwner], $ownerFrame]))))));
function Box<any>($$unnamed~bx : any, $$unnamed~bw : ref) returns ($$unnamed~by : ref);
function Unbox<any>($$unnamed~bz : ref) returns ($$unnamed~ca : any);
axiom (forall<any> x : any, p : ref :: {Unbox(Box(x, p))} (Unbox(Box(x, p)) == x));
function UnboxedType($$unnamed~cb : ref) returns ($$unnamed~cc : name);
axiom (forall p : ref :: {$IsValueType(UnboxedType(p))} ($IsValueType(UnboxedType(p)) ==> (forall<any> heap : <x>[ref, name]x, x : any :: {heap[Box(x, p), $inv]} (IsHeap(heap) ==> ((heap[Box(x, p), $inv] == $typeof(Box(x, p))) && (heap[Box(x, p), $localinv] == $typeof(Box(x, p))))))));
axiom (forall<any> x : any, p : ref :: {(UnboxedType(Box(x, p)) <: System.Object)} (((UnboxedType(Box(x, p)) <: System.Object) && (Box(x, p) == p)) ==> (x == p)));
function BoxTester(p : ref, typ : name) returns ($$unnamed~cd : ref);
axiom (forall p : ref, typ : name :: {BoxTester(p, typ)} ((UnboxedType(p) == typ) <==> (BoxTester(p, typ) != null)));
const System.SByte : name;
axiom $IsValueType(System.SByte);
const System.Byte : name;
axiom $IsValueType(System.Byte);
const System.Int16 : name;
axiom $IsValueType(System.Int16);
const System.UInt16 : name;
axiom $IsValueType(System.UInt16);
const System.Int32 : name;
axiom $IsValueType(System.Int32);
const System.UInt32 : name;
axiom $IsValueType(System.UInt32);
const System.Int64 : name;
axiom $IsValueType(System.Int64);
const System.UInt64 : name;
axiom $IsValueType(System.UInt64);
const System.Char : name;
axiom $IsValueType(System.Char);
const int#m2147483648 : int;
const int#2147483647 : int;
const int#4294967295 : int;
const int#m9223372036854775808 : int;
const int#9223372036854775807 : int;
const int#18446744073709551615 : int;
axiom (int#m9223372036854775808 < int#m2147483648);
axiom (int#m2147483648 < (0 - 100000));
axiom (100000 < int#2147483647);
axiom (int#2147483647 < int#4294967295);
axiom (int#4294967295 < int#9223372036854775807);
axiom (int#9223372036854775807 < int#18446744073709551615);
function InRange(i : int, T : name) returns ($$unnamed~ce : bool);
axiom (forall i : int :: (InRange(i, System.SByte) <==> (((0 - 128) <= i) && (i < 128))));
axiom (forall i : int :: (InRange(i, System.Byte) <==> ((0 <= i) && (i < 256))));
axiom (forall i : int :: (InRange(i, System.Int16) <==> (((0 - 32768) <= i) && (i < 32768))));
axiom (forall i : int :: (InRange(i, System.UInt16) <==> ((0 <= i) && (i < 65536))));
axiom (forall i : int :: (InRange(i, System.Int32) <==> ((int#m2147483648 <= i) && (i <= int#2147483647))));
axiom (forall i : int :: (InRange(i, System.UInt32) <==> ((0 <= i) && (i <= int#4294967295))));
axiom (forall i : int :: (InRange(i, System.Int64) <==> ((int#m9223372036854775808 <= i) && (i <= int#9223372036854775807))));
axiom (forall i : int :: (InRange(i, System.UInt64) <==> ((0 <= i) && (i <= int#18446744073709551615))));
axiom (forall i : int :: (InRange(i, System.Char) <==> ((0 <= i) && (i < 65536))));
function $IntToInt(val : int, fromType : name, toType : name) returns ($$unnamed~cf : int);
function $IntToReal($$unnamed~cg : int, fromType : name, toType : name) returns ($$unnamed~ch : real);
function $RealToInt($$unnamed~ci : real, fromType : name, toType : name) returns ($$unnamed~cj : int);
function $RealToReal(val : real, fromType : name, toType : name) returns ($$unnamed~ck : real);
function $SizeIs($$unnamed~cm : name, $$unnamed~cl : int) returns ($$unnamed~cn : bool);
function $IfThenElse<any>($$unnamed~cq : bool, $$unnamed~cp : any, $$unnamed~co : any) returns ($$unnamed~cr : any);
axiom (forall<any> b : bool, x : any, y : any :: {$IfThenElse(b, x, y)} (b ==> ($IfThenElse(b, x, y) == x)));
axiom (forall<any> b : bool, x : any, y : any :: {$IfThenElse(b, x, y)} (!b ==> ($IfThenElse(b, x, y) == y)));
function #neg($$unnamed~cs : int) returns ($$unnamed~ct : int);
function #and($$unnamed~cv : int, $$unnamed~cu : int) returns ($$unnamed~cw : int);
function #or($$unnamed~cy : int, $$unnamed~cx : int) returns ($$unnamed~cz : int);
function #xor($$unnamed~db : int, $$unnamed~da : int) returns ($$unnamed~dc : int);
function #shl($$unnamed~de : int, $$unnamed~dd : int) returns ($$unnamed~df : int);
function #shr($$unnamed~dh : int, $$unnamed~dg : int) returns ($$unnamed~di : int);
function #rneg($$unnamed~dj : real) returns ($$unnamed~dk : real);
function #radd($$unnamed~dm : real, $$unnamed~dl : real) returns ($$unnamed~dn : real);
function #rsub($$unnamed~dp : real, $$unnamed~do : real) returns ($$unnamed~dq : real);
function #rmul($$unnamed~ds : real, $$unnamed~dr : real) returns ($$unnamed~dt : real);
function #rdiv($$unnamed~dv : real, $$unnamed~du : real) returns ($$unnamed~dw : real);
function #rmod($$unnamed~dy : real, $$unnamed~dx : real) returns ($$unnamed~dz : real);
function #rLess($$unnamed~eb : real, $$unnamed~ea : real) returns ($$unnamed~ec : bool);
function #rAtmost($$unnamed~ee : real, $$unnamed~ed : real) returns ($$unnamed~ef : bool);
function #rEq($$unnamed~eh : real, $$unnamed~eg : real) returns ($$unnamed~ei : bool);
function #rNeq($$unnamed~ek : real, $$unnamed~ej : real) returns ($$unnamed~el : bool);
function #rAtleast($$unnamed~en : real, $$unnamed~em : real) returns ($$unnamed~eo : bool);
function #rGreater($$unnamed~eq : real, $$unnamed~ep : real) returns ($$unnamed~er : bool);
axiom (forall x : int, y : int :: {(x % y)} {(x / y)} ((x % y) == (x - ((x / y) * y))));
axiom (forall x : int, y : int :: {(x % y)} (((0 <= x) && (0 < y)) ==> ((0 <= (x % y)) && ((x % y) < y))));
axiom (forall x : int, y : int :: {(x % y)} (((0 <= x) && (y < 0)) ==> ((0 <= (x % y)) && ((x % y) < (0 - y)))));
axiom (forall x : int, y : int :: {(x % y)} (((x <= 0) && (0 < y)) ==> (((0 - y) < (x % y)) && ((x % y) <= 0))));
axiom (forall x : int, y : int :: {(x % y)} (((x <= 0) && (y < 0)) ==> ((y < (x % y)) && ((x % y) <= 0))));
axiom (forall x : int, y : int :: {((x + y) % y)} (((0 <= x) && (0 <= y)) ==> (((x + y) % y) == (x % y))));
axiom (forall x : int, y : int :: {((y + x) % y)} (((0 <= x) && (0 <= y)) ==> (((y + x) % y) == (x % y))));
axiom (forall x : int, y : int :: {((x - y) % y)} (((0 <= (x - y)) && (0 <= y)) ==> (((x - y) % y) == (x % y))));
axiom (forall a : int, b : int, d : int :: {(a % d), (b % d)} ((((2 <= d) && ((a % d) == (b % d))) && (a < b)) ==> ((a + d) <= b)));
axiom (forall x : int, y : int :: {#and(x, y)} (((0 <= x) || (0 <= y)) ==> (0 <= #and(x, y))));
axiom (forall x : int, y : int :: {#or(x, y)} (((0 <= x) && (0 <= y)) ==> ((0 <= #or(x, y)) && (#or(x, y) <= (x + y)))));
axiom (forall i : int :: {#shl(i, 0)} (#shl(i, 0) == i));
axiom (forall i : int, j : int :: ((0 <= j) ==> (#shl(i, (j + 1)) == (#shl(i, j) * 2))));
axiom (forall i : int :: {#shr(i, 0)} (#shr(i, 0) == i));
axiom (forall i : int, j : int :: ((0 <= j) ==> (#shr(i, (j + 1)) == (#shr(i, j) / 2))));
function #System.String.IsInterned$System.String$notnull($$unnamed~es : ref) returns ($$unnamed~et : ref);
function #System.String.Equals$System.String($$unnamed~ev : ref, $$unnamed~eu : ref) returns ($$unnamed~ew : bool);
function #System.String.Equals$System.String$System.String($$unnamed~ey : ref, $$unnamed~ex : ref) returns ($$unnamed~ez : bool);
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String(a, b)} (#System.String.Equals$System.String(a, b) == #System.String.Equals$System.String$System.String(a, b)));
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String$System.String(a, b)} (#System.String.Equals$System.String$System.String(a, b) == #System.String.Equals$System.String$System.String(b, a)));
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String$System.String(a, b)} ((((a != null) && (b != null)) && #System.String.Equals$System.String$System.String(a, b)) ==> (#System.String.IsInterned$System.String$notnull(a) == #System.String.IsInterned$System.String$notnull(b))));
const $UnknownRef : ref;
const C.s : name;
const D.t : name;
const T.y : name;
const S.z : name;
const S.x : name;
const U.u : name;
const C.o : name;
const C.x : name;
const C.arr : name;
const S.w : name;
const System.Runtime.InteropServices._Type : name;
const System.Boolean : name;
const System.Reflection.IReflect : name;
const System.Exception : name;
const S : name;
const D : name;
const Microsoft.Contracts.GuardException : name;
const System.Runtime.Serialization.ISerializable : name;
const Microsoft.Contracts.ICheckedException : name;
const System.IComparable : name;
const System.ICloneable : name;
const System.Reflection.ICustomAttributeProvider : name;
const System.IConvertible : name;
const System.Collections.Generic.IEnumerable`1...System.Char : name;
const Microsoft.Contracts.ObjectInvariantException : name;
const System.IEquatable`1...System.String : name;
const System.IComparable`1...System.String : name;
const U : name;
const Iface : name;
const System.Runtime.InteropServices._MemberInfo : name;
const System.Reflection.MemberInfo : name;
const T : name;
const System.Runtime.InteropServices._Exception : name;
const System.Collections.IEnumerable : name;
const C : name;
axiom !IsStaticField(C.x);
axiom IsDirectlyModifiableField(C.x);
axiom (DeclType(C.x) == C);
axiom (AsRangeField(C.x, System.Int32) == C.x);
axiom !IsStaticField(C.s);
axiom IsDirectlyModifiableField(C.s);
axiom (DeclType(C.s) == C);
axiom (AsNonNullRefField(C.s, System.String) == C.s);
axiom !IsStaticField(C.arr);
axiom IsDirectlyModifiableField(C.arr);
axiom (DeclType(C.arr) == C);
axiom (AsRefField(C.arr, ValueArray(System.Int32, 1)) == C.arr);
axiom !IsStaticField(C.o);
axiom IsDirectlyModifiableField(C.o);
axiom (DeclType(C.o) == C);
axiom (AsNonNullRefField(C.o, System.Object) == C.o);
axiom !IsStaticField(S.x);
axiom IsDirectlyModifiableField(S.x);
axiom (DeclType(S.x) == S);
axiom (AsRangeField(S.x, System.Int32) == S.x);
axiom !IsStaticField(S.z);
axiom IsDirectlyModifiableField(S.z);
axiom (DeclType(S.z) == S);
axiom (AsRangeField(S.z, System.Int32) == S.z);
axiom !IsStaticField(S.w);
axiom IsDirectlyModifiableField(S.w);
axiom (DeclType(S.w) == S);
axiom (AsRangeField(S.w, System.Int32) == S.w);
axiom !IsStaticField(T.y);
axiom IsDirectlyModifiableField(T.y);
axiom (DeclType(T.y) == T);
axiom (AsRangeField(T.y, System.Int32) == T.y);
axiom !IsStaticField(U.u);
axiom IsDirectlyModifiableField(U.u);
axiom (DeclType(U.u) == U);
axiom (AsRangeField(U.u, System.Int32) == U.u);
axiom !IsStaticField(D.t);
axiom IsDirectlyModifiableField(D.t);
axiom (DeclType(D.t) == D);
axiom (AsNonNullRefField(D.t, T) == D.t);
axiom (Iface <: System.Object);
axiom $IsMemberlessType(Iface);
axiom (C <: C);
axiom ($BaseClass(C) == System.Object);
axiom ((C <: $BaseClass(C)) && (AsDirectSubClass(C, $BaseClass(C)) == C));
axiom (!$IsImmutable(C) && ($AsMutable(C) == C));
axiom (C <: Iface);
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: C)} (((IsHeap($h) && ($h[$oi, $inv] <: C)) && ($h[$oi, $localinv] != System.Object)) ==> (0 <= $h[$oi, C.x])));
axiom (forall $U : name :: {($U <: System.Boolean)} (($U <: System.Boolean) ==> ($U == System.Boolean)));
procedure C.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation C.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var stack0i : int;
  var stack1i : int;
  var stack0b : bool;
  var local0 : bool where true;
  var stack50000o : ref;
  var stack0o : ref;
  var SS$Display.Return.Local : bool where true;
  entry: assume $IsNotNull(this, C); goto $$entry~b;
  $$entry~b: assume ($Heap[this, $allocated] == true); goto $$entry~a;
  $$entry~a: throwException := throwException$in; goto block2091;
  block2091: goto block2108;
  block2108: stack0i := 0; goto $$block2108~b;
  $$block2108~b: assert (this != null); goto $$block2108~a;
  $$block2108~a: stack1i := $Heap[this, C.x]; goto true2108to2210, false2108to2125;
  true2108to2210: assume (stack0i <= stack1i); goto block2210;
  false2108to2125: assume (stack0i > stack1i); goto block2125;
  block2210: local0 := true; goto block2227;
  block2125: stack0b := throwException; goto true2125to2176, false2125to2142;
  true2125to2176: assume !stack0b; goto block2176;
  false2125to2142: assume stack0b; goto block2142;
  block2176: local0 := false; goto block2227;
  block2142: assume false; goto $$block2142~i;
  $$block2142~i: havoc stack50000o; goto $$block2142~h;
  $$block2142~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block2142~g;
  $$block2142~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block2142~f;
  $$block2142~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block2142~e;
  $$block2142~e: assert (stack50000o != null); goto $$block2142~d;
  $$block2142~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block2142~c;
  $$block2142~c: stack0o := stack50000o; goto $$block2142~b;
  $$block2142~b: assert (stack0o != null); goto $$block2142~a;
  $$block2142~a: assume false; return;
  block2227: SS$Display.Return.Local := local0; goto $$block2227~b;
  $$block2227~b: stack0b := local0; goto $$block2227~a;
  $$block2227~a: $result := stack0b; return;
  
}

axiom (Microsoft.Contracts.ObjectInvariantException <: Microsoft.Contracts.ObjectInvariantException);
axiom (Microsoft.Contracts.GuardException <: Microsoft.Contracts.GuardException);
axiom (System.Exception <: System.Exception);
axiom ($BaseClass(System.Exception) == System.Object);
axiom ((System.Exception <: $BaseClass(System.Exception)) && (AsDirectSubClass(System.Exception, $BaseClass(System.Exception)) == System.Exception));
axiom (!$IsImmutable(System.Exception) && ($AsMutable(System.Exception) == System.Exception));
axiom (System.Runtime.Serialization.ISerializable <: System.Object);
axiom $IsMemberlessType(System.Runtime.Serialization.ISerializable);
axiom (System.Exception <: System.Runtime.Serialization.ISerializable);
axiom (System.Runtime.InteropServices._Exception <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._Exception);
axiom (System.Exception <: System.Runtime.InteropServices._Exception);
axiom ($BaseClass(Microsoft.Contracts.GuardException) == System.Exception);
axiom ((Microsoft.Contracts.GuardException <: $BaseClass(Microsoft.Contracts.GuardException)) && (AsDirectSubClass(Microsoft.Contracts.GuardException, $BaseClass(Microsoft.Contracts.GuardException)) == Microsoft.Contracts.GuardException));
axiom (!$IsImmutable(Microsoft.Contracts.GuardException) && ($AsMutable(Microsoft.Contracts.GuardException) == Microsoft.Contracts.GuardException));
axiom ($BaseClass(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.GuardException);
axiom ((Microsoft.Contracts.ObjectInvariantException <: $BaseClass(Microsoft.Contracts.ObjectInvariantException)) && (AsDirectSubClass(Microsoft.Contracts.ObjectInvariantException, $BaseClass(Microsoft.Contracts.ObjectInvariantException)) == Microsoft.Contracts.ObjectInvariantException));
axiom (!$IsImmutable(Microsoft.Contracts.ObjectInvariantException) && ($AsMutable(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.ObjectInvariantException));
procedure Microsoft.Contracts.ObjectInvariantException..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == Microsoft.Contracts.ObjectInvariantException)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(Microsoft.Contracts.ObjectInvariantException <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

procedure C.M0(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation C.M0(this : ref) {
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : int where InRange(local3, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  entry: assume $IsNotNull(this, C); goto $$entry~c;
  $$entry~c: assume ($Heap[this, $allocated] == true); goto block2975;
  block2975: goto block3128;
  block3128: temp0 := this; goto $$block3128~g;
  $$block3128~g: assert (temp0 != null); goto $$block3128~f;
  $$block3128~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == C)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block3128~e;
  $$block3128~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block3128~d;
  $$block3128~d: havoc temp1; goto $$block3128~c;
  $$block3128~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block3128~b;
  $$block3128~b: assume IsHeap($Heap); goto $$block3128~a;
  $$block3128~a: local2 := null; goto block3145;
  block3145: assert (this != null); goto $$block3145~h;
  $$block3145~h: local3 := $Heap[this, C.x]; goto $$block3145~g;
  $$block3145~g: stack0i := 1; goto $$block3145~f;
  $$block3145~f: stack0i := (local3 + stack0i); goto $$block3145~e;
  $$block3145~e: assert (this != null); goto $$block3145~d;
  $$block3145~d: assert (!($Heap[this, $inv] <: C) || ($Heap[this, $localinv] == System.Object)); goto $$block3145~c;
  $$block3145~c: $Heap := $Heap[this, C.x := stack0i]; goto $$block3145~b;
  $$block3145~b: assume IsHeap($Heap); goto $$block3145~a;
  $$block3145~a: stack0i := local3; goto block3230;
  block3230: stack0o := null; goto true3230to3298, false3230to3247;
  true3230to3298: assume (local2 == stack0o); goto block3298;
  false3230to3247: assume (local2 != stack0o); goto block3247;
  block3298: assert (temp0 != null); goto $$block3298~e;
  $$block3298~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block3298~d;
  $$block3298~d: assert (0 <= $Heap[temp0, C.x]); goto $$block3298~c;
  $$block3298~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == C)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block3298~b;
  $$block3298~b: $Heap := $Heap[temp0, $inv := C]; goto $$block3298~a;
  $$block3298~a: assume IsHeap($Heap); goto block3281;
  block3247: goto true3247to3298, false3247to3264;
  true3247to3298: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block3298;
  false3247to3264: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block3264;
  block3264: goto block3281;
  block3281: goto block3196;
  block3196: return;
  
}

axiom (Microsoft.Contracts.ICheckedException <: System.Object);
axiom $IsMemberlessType(Microsoft.Contracts.ICheckedException);
procedure C.M1(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation C.M1(this : ref) {
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : int where InRange(local3, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, C); goto $$entry~d;
  $$entry~d: assume ($Heap[this, $allocated] == true); goto block4573;
  block4573: goto block4726;
  block4726: temp0 := this; goto $$block4726~j;
  $$block4726~j: havoc stack1s; goto $$block4726~i;
  $$block4726~i: assume $IsTokenForType(stack1s, C); goto $$block4726~h;
  $$block4726~h: stack1o := TypeObject(C); goto $$block4726~g;
  $$block4726~g: assert (temp0 != null); goto $$block4726~f;
  $$block4726~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: C)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block4726~e;
  $$block4726~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block4726~d;
  $$block4726~d: havoc temp1; goto $$block4726~c;
  $$block4726~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block4726~b;
  $$block4726~b: assume IsHeap($Heap); goto $$block4726~a;
  $$block4726~a: local2 := null; goto block4743;
  block4743: assert (this != null); goto $$block4743~h;
  $$block4743~h: local3 := $Heap[this, C.x]; goto $$block4743~g;
  $$block4743~g: stack0i := 1; goto $$block4743~f;
  $$block4743~f: stack0i := (local3 + stack0i); goto $$block4743~e;
  $$block4743~e: assert (this != null); goto $$block4743~d;
  $$block4743~d: assert (!($Heap[this, $inv] <: C) || ($Heap[this, $localinv] == System.Object)); goto $$block4743~c;
  $$block4743~c: $Heap := $Heap[this, C.x := stack0i]; goto $$block4743~b;
  $$block4743~b: assume IsHeap($Heap); goto $$block4743~a;
  $$block4743~a: stack0i := local3; goto block4828;
  block4828: stack0o := null; goto true4828to4896, false4828to4845;
  true4828to4896: assume (local2 == stack0o); goto block4896;
  false4828to4845: assume (local2 != stack0o); goto block4845;
  block4896: havoc stack0s; goto $$block4896~h;
  $$block4896~h: assume $IsTokenForType(stack0s, C); goto $$block4896~g;
  $$block4896~g: stack0o := TypeObject(C); goto $$block4896~f;
  $$block4896~f: assert (temp0 != null); goto $$block4896~e;
  $$block4896~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block4896~d;
  $$block4896~d: assert (0 <= $Heap[temp0, C.x]); goto $$block4896~c;
  $$block4896~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == C)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block4896~b;
  $$block4896~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block4896~a;
  $$block4896~a: assume IsHeap($Heap); goto block4879;
  block4845: goto true4845to4896, false4845to4862;
  true4845to4896: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block4896;
  false4845to4862: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block4862;
  block4862: goto block4879;
  block4879: goto block4794;
  block4794: return;
  
}

axiom (System.Type <: System.Type);
axiom (System.Reflection.MemberInfo <: System.Reflection.MemberInfo);
axiom ($BaseClass(System.Reflection.MemberInfo) == System.Object);
axiom ((System.Reflection.MemberInfo <: $BaseClass(System.Reflection.MemberInfo)) && (AsDirectSubClass(System.Reflection.MemberInfo, $BaseClass(System.Reflection.MemberInfo)) == System.Reflection.MemberInfo));
axiom ($IsImmutable(System.Reflection.MemberInfo) && ($AsImmutable(System.Reflection.MemberInfo) == System.Reflection.MemberInfo));
axiom (System.Reflection.ICustomAttributeProvider <: System.Object);
axiom $IsMemberlessType(System.Reflection.ICustomAttributeProvider);
axiom (System.Reflection.MemberInfo <: System.Reflection.ICustomAttributeProvider);
axiom (System.Runtime.InteropServices._MemberInfo <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._MemberInfo);
axiom (System.Reflection.MemberInfo <: System.Runtime.InteropServices._MemberInfo);
axiom $IsMemberlessType(System.Reflection.MemberInfo);
axiom ($BaseClass(System.Type) == System.Reflection.MemberInfo);
axiom ((System.Type <: $BaseClass(System.Type)) && (AsDirectSubClass(System.Type, $BaseClass(System.Type)) == System.Type));
axiom ($IsImmutable(System.Type) && ($AsImmutable(System.Type) == System.Type));
axiom (System.Runtime.InteropServices._Type <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._Type);
axiom (System.Type <: System.Runtime.InteropServices._Type);
axiom (System.Reflection.IReflect <: System.Object);
axiom $IsMemberlessType(System.Reflection.IReflect);
axiom (System.Type <: System.Reflection.IReflect);
axiom $IsMemberlessType(System.Type);
procedure C.M2(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation C.M2(this : ref) {
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : int where InRange(local3, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, C); goto $$entry~e;
  $$entry~e: assume ($Heap[this, $allocated] == true); goto block6001;
  block6001: goto block6154;
  block6154: temp0 := this; goto $$block6154~j;
  $$block6154~j: havoc stack1s; goto $$block6154~i;
  $$block6154~i: assume $IsTokenForType(stack1s, C); goto $$block6154~h;
  $$block6154~h: stack1o := TypeObject(C); goto $$block6154~g;
  $$block6154~g: assert (temp0 != null); goto $$block6154~f;
  $$block6154~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: C)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block6154~e;
  $$block6154~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block6154~d;
  $$block6154~d: havoc temp1; goto $$block6154~c;
  $$block6154~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block6154~b;
  $$block6154~b: assume IsHeap($Heap); goto $$block6154~a;
  $$block6154~a: local2 := null; goto block6171;
  block6171: assert (this != null); goto $$block6171~h;
  $$block6171~h: local3 := $Heap[this, C.x]; goto $$block6171~g;
  $$block6171~g: stack0i := 1; goto $$block6171~f;
  $$block6171~f: stack0i := (local3 - stack0i); goto $$block6171~e;
  $$block6171~e: assert (this != null); goto $$block6171~d;
  $$block6171~d: assert (!($Heap[this, $inv] <: C) || ($Heap[this, $localinv] == System.Object)); goto $$block6171~c;
  $$block6171~c: $Heap := $Heap[this, C.x := stack0i]; goto $$block6171~b;
  $$block6171~b: assume IsHeap($Heap); goto $$block6171~a;
  $$block6171~a: stack0i := local3; goto block6256;
  block6256: stack0o := null; goto true6256to6324, false6256to6273;
  true6256to6324: assume (local2 == stack0o); goto block6324;
  false6256to6273: assume (local2 != stack0o); goto block6273;
  block6324: havoc stack0s; goto $$block6324~h;
  $$block6324~h: assume $IsTokenForType(stack0s, C); goto $$block6324~g;
  $$block6324~g: stack0o := TypeObject(C); goto $$block6324~f;
  $$block6324~f: assert (temp0 != null); goto $$block6324~e;
  $$block6324~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block6324~d;
  $$block6324~d: assert (0 <= $Heap[temp0, C.x]); goto $$block6324~c;
  $$block6324~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == C)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block6324~b;
  $$block6324~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block6324~a;
  $$block6324~a: assume IsHeap($Heap); goto block6307;
  block6273: goto true6273to6324, false6273to6290;
  true6273to6324: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block6324;
  false6273to6290: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block6290;
  block6290: goto block6307;
  block6307: goto block6222;
  block6222: return;
  
}

procedure C.M3(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation C.M3(this : ref) {
  var local1 : ref where $Is(local1, System.Object);
  var stack0o : ref;
  var stack1s : struct;
  var stack1o : ref;
  var local2 : int where InRange(local2, System.Int32);
  var stack0i : int;
  entry: assume $IsNotNull(this, C); goto $$entry~f;
  $$entry~f: assume ($Heap[this, $allocated] == true); goto block7259;
  block7259: goto block7412;
  block7412: local1 := this; goto $$block7412~g;
  $$block7412~g: stack0o := local1; goto $$block7412~f;
  $$block7412~f: havoc stack1s; goto $$block7412~e;
  $$block7412~e: assume $IsTokenForType(stack1s, System.Object); goto $$block7412~d;
  $$block7412~d: stack1o := TypeObject(System.Object); goto $$block7412~c;
  $$block7412~c: assert (stack0o != null); goto $$block7412~b;
  $$block7412~b: assert ((((($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack0o, $ownerRef], $inv] <: $Heap[stack0o, $ownerFrame])) || ($Heap[$Heap[stack0o, $ownerRef], $localinv] == $BaseClass($Heap[stack0o, $ownerFrame]))) && ($Heap[stack0o, $inv] <: System.Object)) && ($Heap[stack0o, $localinv] == $typeof(stack0o))); goto $$block7412~a;
  $$block7412~a: assert false; goto block7429;
  block7429: assert (this != null); goto $$block7429~h;
  $$block7429~h: local2 := $Heap[this, C.x]; goto $$block7429~g;
  $$block7429~g: stack0i := 1; goto $$block7429~f;
  $$block7429~f: stack0i := (local2 + stack0i); goto $$block7429~e;
  $$block7429~e: assert (this != null); goto $$block7429~d;
  $$block7429~d: assert (!($Heap[this, $inv] <: C) || ($Heap[this, $localinv] == System.Object)); goto $$block7429~c;
  $$block7429~c: $Heap := $Heap[this, C.x := stack0i]; goto $$block7429~b;
  $$block7429~b: assume IsHeap($Heap); goto $$block7429~a;
  $$block7429~a: stack0i := local2; goto block7480;
  block7480: stack0o := local1; goto $$block7480~e;
  $$block7480~e: havoc stack1s; goto $$block7480~d;
  $$block7480~d: assume $IsTokenForType(stack1s, System.Object); goto $$block7480~c;
  $$block7480~c: stack1o := TypeObject(System.Object); goto $$block7480~b;
  $$block7480~b: assert (stack0o != null); goto $$block7480~a;
  $$block7480~a: assert false; goto block7446;
  block7446: return;
  
}

procedure C.M5(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation C.M5(this : ref) {
  var local1 : ref where $Is(local1, System.String);
  var stack0o : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp0 : exposeVersionType;
  entry: assume $IsNotNull(this, C); goto $$entry~g;
  $$entry~g: assume ($Heap[this, $allocated] == true); goto block8126;
  block8126: goto block8279;
  block8279: assert (this != null); goto $$block8279~g;
  $$block8279~g: local1 := $Heap[this, C.s]; goto $$block8279~f;
  $$block8279~f: stack0o := local1; goto $$block8279~e;
  $$block8279~e: havoc stack1s; goto $$block8279~d;
  $$block8279~d: assume $IsTokenForType(stack1s, System.String); goto $$block8279~c;
  $$block8279~c: stack1o := TypeObject(System.String); goto $$block8279~b;
  $$block8279~b: assert (stack0o != null); goto $$block8279~a;
  $$block8279~a: assert false; goto block8296;
  block8296: stack0o := $stringLiteral0; goto $$block8296~e;
  $$block8296~e: assert (this != null); goto $$block8296~d;
  $$block8296~d: havoc temp0; goto $$block8296~c;
  $$block8296~c: $Heap := $Heap[this, $exposeVersion := temp0]; goto $$block8296~b;
  $$block8296~b: $Heap := $Heap[this, C.s := stack0o]; goto $$block8296~a;
  $$block8296~a: assume IsHeap($Heap); goto block8347;
  block8347: stack0o := local1; goto $$block8347~e;
  $$block8347~e: havoc stack1s; goto $$block8347~d;
  $$block8347~d: assume $IsTokenForType(stack1s, System.String); goto $$block8347~c;
  $$block8347~c: stack1o := TypeObject(System.String); goto $$block8347~b;
  $$block8347~b: assert (stack0o != null); goto $$block8347~a;
  $$block8347~a: assert false; goto block8313;
  block8313: return;
  
}

axiom (System.String <: System.String);
axiom ($BaseClass(System.String) == System.Object);
axiom ((System.String <: $BaseClass(System.String)) && (AsDirectSubClass(System.String, $BaseClass(System.String)) == System.String));
axiom ($IsImmutable(System.String) && ($AsImmutable(System.String) == System.String));
axiom (System.IComparable <: System.Object);
axiom $IsMemberlessType(System.IComparable);
axiom (System.String <: System.IComparable);
axiom (System.ICloneable <: System.Object);
axiom $IsMemberlessType(System.ICloneable);
axiom (System.String <: System.ICloneable);
axiom (System.IConvertible <: System.Object);
axiom $IsMemberlessType(System.IConvertible);
axiom (System.String <: System.IConvertible);
axiom (System.IComparable`1...System.String <: System.Object);
axiom $IsMemberlessType(System.IComparable`1...System.String);
axiom (System.String <: System.IComparable`1...System.String);
axiom (System.Collections.Generic.IEnumerable`1...System.Char <: System.Object);
axiom (System.Collections.IEnumerable <: System.Object);
axiom $IsMemberlessType(System.Collections.IEnumerable);
axiom (System.Collections.Generic.IEnumerable`1...System.Char <: System.Collections.IEnumerable);
axiom $IsMemberlessType(System.Collections.Generic.IEnumerable`1...System.Char);
axiom (System.String <: System.Collections.Generic.IEnumerable`1...System.Char);
axiom (System.String <: System.Collections.IEnumerable);
axiom (System.IEquatable`1...System.String <: System.Object);
axiom $IsMemberlessType(System.IEquatable`1...System.String);
axiom (System.String <: System.IEquatable`1...System.String);
axiom (forall $U : name :: {($U <: System.String)} (($U <: System.String) ==> ($U == System.String)));
procedure C.M6(this : ref);
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == C)) && ($Heap[this, $localinv] == $typeof(this)));
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation C.M6(this : ref) {
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var temp2 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp3 : exposeVersionType;
  var local4 : ref where $Is(local4, System.Exception);
  var local5 : int where InRange(local5, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, C); goto $$entry~h;
  $$entry~h: assume ($Heap[this, $allocated] == true); goto block9401;
  block9401: goto block9605;
  block9605: temp0 := this; goto $$block9605~g;
  $$block9605~g: assert (temp0 != null); goto $$block9605~f;
  $$block9605~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == C)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block9605~e;
  $$block9605~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block9605~d;
  $$block9605~d: havoc temp1; goto $$block9605~c;
  $$block9605~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block9605~b;
  $$block9605~b: assume IsHeap($Heap); goto $$block9605~a;
  $$block9605~a: local2 := null; goto block9622;
  block9622: temp2 := this; goto $$block9622~j;
  $$block9622~j: havoc stack1s; goto $$block9622~i;
  $$block9622~i: assume $IsTokenForType(stack1s, C); goto $$block9622~h;
  $$block9622~h: stack1o := TypeObject(C); goto $$block9622~g;
  $$block9622~g: assert (temp2 != null); goto $$block9622~f;
  $$block9622~f: assert ((((($Heap[temp2, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp2, $ownerRef], $inv] <: $Heap[temp2, $ownerFrame])) || ($Heap[$Heap[temp2, $ownerRef], $localinv] == $BaseClass($Heap[temp2, $ownerFrame]))) && ($Heap[temp2, $inv] <: C)) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block9622~e;
  $$block9622~e: $Heap := $Heap[temp2, $localinv := System.Object]; goto $$block9622~d;
  $$block9622~d: havoc temp3; goto $$block9622~c;
  $$block9622~c: $Heap := $Heap[temp2, $exposeVersion := temp3]; goto $$block9622~b;
  $$block9622~b: assume IsHeap($Heap); goto $$block9622~a;
  $$block9622~a: local4 := null; goto block9639;
  block9639: assert (this != null); goto $$block9639~h;
  $$block9639~h: local5 := $Heap[this, C.x]; goto $$block9639~g;
  $$block9639~g: stack0i := 1; goto $$block9639~f;
  $$block9639~f: stack0i := (local5 + stack0i); goto $$block9639~e;
  $$block9639~e: assert (this != null); goto $$block9639~d;
  $$block9639~d: assert (!($Heap[this, $inv] <: C) || ($Heap[this, $localinv] == System.Object)); goto $$block9639~c;
  $$block9639~c: $Heap := $Heap[this, C.x := stack0i]; goto $$block9639~b;
  $$block9639~b: assume IsHeap($Heap); goto $$block9639~a;
  $$block9639~a: stack0i := local5; goto block9775;
  block9775: stack0o := null; goto true9775to9843, false9775to9792;
  true9775to9843: assume (local4 == stack0o); goto block9843;
  false9775to9792: assume (local4 != stack0o); goto block9792;
  block9843: havoc stack0s; goto $$block9843~h;
  $$block9843~h: assume $IsTokenForType(stack0s, C); goto $$block9843~g;
  $$block9843~g: stack0o := TypeObject(C); goto $$block9843~f;
  $$block9843~f: assert (temp2 != null); goto $$block9843~e;
  $$block9843~e: assert ($Heap[temp2, $localinv] == System.Object); goto $$block9843~d;
  $$block9843~d: assert (0 <= $Heap[temp2, C.x]); goto $$block9843~c;
  $$block9843~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp2)) && ($Heap[$p, $ownerFrame] == C)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block9843~b;
  $$block9843~b: $Heap := $Heap[temp2, $localinv := $typeof(temp2)]; goto $$block9843~a;
  $$block9843~a: assume IsHeap($Heap); goto block9826;
  block9792: goto true9792to9843, false9792to9809;
  true9792to9843: assume ($As(local4, Microsoft.Contracts.ICheckedException) != null); goto block9843;
  false9792to9809: assume ($As(local4, Microsoft.Contracts.ICheckedException) == null); goto block9809;
  block9809: goto block9826;
  block9826: goto block9690;
  block9690: goto block9945;
  block9945: stack0o := null; goto true9945to10013, false9945to9962;
  true9945to10013: assume (local2 == stack0o); goto block10013;
  false9945to9962: assume (local2 != stack0o); goto block9962;
  block10013: assert (temp0 != null); goto $$block10013~e;
  $$block10013~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block10013~d;
  $$block10013~d: assert (0 <= $Heap[temp0, C.x]); goto $$block10013~c;
  $$block10013~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == C)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block10013~b;
  $$block10013~b: $Heap := $Heap[temp0, $inv := C]; goto $$block10013~a;
  $$block10013~a: assume IsHeap($Heap); goto block9996;
  block9962: goto true9962to10013, false9962to9979;
  true9962to10013: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block10013;
  false9962to9979: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block9979;
  block9979: goto block9996;
  block9996: goto block9741;
  block9741: return;
  
}

procedure C.M7(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation C.M7(this : ref) {
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var temp2 : ref;
  var temp3 : exposeVersionType;
  var local4 : ref where $Is(local4, System.Exception);
  var local5 : int where InRange(local5, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, C); goto $$entry~i;
  $$entry~i: assume ($Heap[this, $allocated] == true); goto block11730;
  block11730: goto block11883;
  block11883: temp0 := this; goto $$block11883~j;
  $$block11883~j: havoc stack1s; goto $$block11883~i;
  $$block11883~i: assume $IsTokenForType(stack1s, C); goto $$block11883~h;
  $$block11883~h: stack1o := TypeObject(C); goto $$block11883~g;
  $$block11883~g: assert (temp0 != null); goto $$block11883~f;
  $$block11883~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: C)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block11883~e;
  $$block11883~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block11883~d;
  $$block11883~d: havoc temp1; goto $$block11883~c;
  $$block11883~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block11883~b;
  $$block11883~b: assume IsHeap($Heap); goto $$block11883~a;
  $$block11883~a: local2 := null; goto block11900;
  block11900: temp2 := this; goto $$block11900~g;
  $$block11900~g: assert (temp2 != null); goto $$block11900~f;
  $$block11900~f: assert ((((($Heap[temp2, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp2, $ownerRef], $inv] <: $Heap[temp2, $ownerFrame])) || ($Heap[$Heap[temp2, $ownerRef], $localinv] == $BaseClass($Heap[temp2, $ownerFrame]))) && ($Heap[temp2, $inv] == C)) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block11900~e;
  $$block11900~e: $Heap := $Heap[temp2, $inv := System.Object]; goto $$block11900~d;
  $$block11900~d: havoc temp3; goto $$block11900~c;
  $$block11900~c: $Heap := $Heap[temp2, $exposeVersion := temp3]; goto $$block11900~b;
  $$block11900~b: assume IsHeap($Heap); goto $$block11900~a;
  $$block11900~a: local4 := null; goto block11917;
  block11917: assert (this != null); goto $$block11917~h;
  $$block11917~h: local5 := $Heap[this, C.x]; goto $$block11917~g;
  $$block11917~g: stack0i := 1; goto $$block11917~f;
  $$block11917~f: stack0i := (local5 + stack0i); goto $$block11917~e;
  $$block11917~e: assert (this != null); goto $$block11917~d;
  $$block11917~d: assert (!($Heap[this, $inv] <: C) || ($Heap[this, $localinv] == System.Object)); goto $$block11917~c;
  $$block11917~c: $Heap := $Heap[this, C.x := stack0i]; goto $$block11917~b;
  $$block11917~b: assume IsHeap($Heap); goto $$block11917~a;
  $$block11917~a: stack0i := local5; goto block12053;
  block12053: stack0o := null; goto true12053to12121, false12053to12070;
  true12053to12121: assume (local4 == stack0o); goto block12121;
  false12053to12070: assume (local4 != stack0o); goto block12070;
  block12121: assert (temp2 != null); goto $$block12121~e;
  $$block12121~e: assert (($Heap[temp2, $inv] == System.Object) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block12121~d;
  $$block12121~d: assert (0 <= $Heap[temp2, C.x]); goto $$block12121~c;
  $$block12121~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp2)) && ($Heap[$p, $ownerFrame] == C)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block12121~b;
  $$block12121~b: $Heap := $Heap[temp2, $inv := C]; goto $$block12121~a;
  $$block12121~a: assume IsHeap($Heap); goto block12104;
  block12070: goto true12070to12121, false12070to12087;
  true12070to12121: assume ($As(local4, Microsoft.Contracts.ICheckedException) != null); goto block12121;
  false12070to12087: assume ($As(local4, Microsoft.Contracts.ICheckedException) == null); goto block12087;
  block12087: goto block12104;
  block12104: goto block11968;
  block11968: goto block12223;
  block12223: stack0o := null; goto true12223to12291, false12223to12240;
  true12223to12291: assume (local2 == stack0o); goto block12291;
  false12223to12240: assume (local2 != stack0o); goto block12240;
  block12291: havoc stack0s; goto $$block12291~h;
  $$block12291~h: assume $IsTokenForType(stack0s, C); goto $$block12291~g;
  $$block12291~g: stack0o := TypeObject(C); goto $$block12291~f;
  $$block12291~f: assert (temp0 != null); goto $$block12291~e;
  $$block12291~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block12291~d;
  $$block12291~d: assert (0 <= $Heap[temp0, C.x]); goto $$block12291~c;
  $$block12291~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == C)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block12291~b;
  $$block12291~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block12291~a;
  $$block12291~a: assume IsHeap($Heap); goto block12274;
  block12240: goto true12240to12291, false12240to12257;
  true12240to12291: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block12291;
  false12240to12257: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block12257;
  block12257: goto block12274;
  block12274: goto block12019;
  block12019: return;
  
}

procedure C..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == C)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(C <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation C..ctor(this : ref) {
  var stack50000o : ref;
  var stack0o : ref;
  var temp0 : exposeVersionType;
  var temp1 : exposeVersionType;
  var stack0i : int;
  var temp2 : exposeVersionType;
  var temp3 : ref;
  entry: assume $IsNotNull(this, C); goto $$entry~m;
  $$entry~m: assume ($Heap[this, $allocated] == true); goto $$entry~l;
  $$entry~l: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~k;
  $$entry~k: assume ($Heap[this, C.arr] == null); goto $$entry~j;
  $$entry~j: assume ($Heap[this, C.x] == 0); goto block13515;
  block13515: goto block13532;
  block13532: havoc stack50000o; goto $$block13532~ah;
  $$block13532~ah: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == System.Object)); goto $$block13532~ag;
  $$block13532~ag: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block13532~af;
  $$block13532~af: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block13532~ae;
  $$block13532~ae: assert (stack50000o != null); goto $$block13532~ad;
  $$block13532~ad: call System.Object..ctor(stack50000o); goto $$block13532~ac;
  $$block13532~ac: stack0o := stack50000o; goto $$block13532~ab;
  $$block13532~ab: assert (this != null); goto $$block13532~aa;
  $$block13532~aa: havoc temp0; goto $$block13532~z;
  $$block13532~z: $Heap := $Heap[this, $exposeVersion := temp0]; goto $$block13532~y;
  $$block13532~y: $Heap := $Heap[this, C.o := stack0o]; goto $$block13532~x;
  $$block13532~x: assume IsHeap($Heap); goto $$block13532~w;
  $$block13532~w: stack0o := $stringLiteral1; goto $$block13532~v;
  $$block13532~v: assert (this != null); goto $$block13532~u;
  $$block13532~u: havoc temp1; goto $$block13532~t;
  $$block13532~t: $Heap := $Heap[this, $exposeVersion := temp1]; goto $$block13532~s;
  $$block13532~s: $Heap := $Heap[this, C.s := stack0o]; goto $$block13532~r;
  $$block13532~r: assume IsHeap($Heap); goto $$block13532~q;
  $$block13532~q: stack0i := 3; goto $$block13532~p;
  $$block13532~p: assert (0 <= stack0i); goto $$block13532~o;
  $$block13532~o: havoc stack0o; goto $$block13532~n;
  $$block13532~n: assume (($Heap[stack0o, $allocated] == false) && ($Length(stack0o) == stack0i)); goto $$block13532~m;
  $$block13532~m: assume $IsNotNull(stack0o, ValueArray(System.Int32, 1)); goto $$block13532~l;
  $$block13532~l: assume (($Heap[stack0o, $ownerRef] == stack0o) && ($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block13532~k;
  $$block13532~k: assume ((($Heap[stack0o, $inv] == ValueArray(System.Int32, 1)) && ($Heap[stack0o, $localinv] == ValueArray(System.Int32, 1))) && ((($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack0o, $ownerRef], $inv] <: $Heap[stack0o, $ownerFrame])) || ($Heap[$Heap[stack0o, $ownerRef], $localinv] == $BaseClass($Heap[stack0o, $ownerFrame])))); goto $$block13532~j;
  $$block13532~j: assume (forall $i : int :: (ValueArrayGet($Heap[stack0o, $elements], $i) == 0)); goto $$block13532~i;
  $$block13532~i: $Heap := $Heap[stack0o, $allocated := true]; goto $$block13532~h;
  $$block13532~h: assume IsHeap($Heap); goto $$block13532~g;
  $$block13532~g: assert (this != null); goto $$block13532~f;
  $$block13532~f: havoc temp2; goto $$block13532~e;
  $$block13532~e: $Heap := $Heap[this, $exposeVersion := temp2]; goto $$block13532~d;
  $$block13532~d: $Heap := $Heap[this, C.arr := stack0o]; goto $$block13532~c;
  $$block13532~c: assume IsHeap($Heap); goto $$block13532~b;
  $$block13532~b: assert (this != null); goto $$block13532~a;
  $$block13532~a: call System.Object..ctor(this); goto block13600;
  block13600: temp3 := this; goto $$block13600~f;
  $$block13600~f: assert (temp3 != null); goto $$block13600~e;
  $$block13600~e: assert (($Heap[temp3, $inv] == System.Object) && ($Heap[temp3, $localinv] == $typeof(temp3))); goto $$block13600~d;
  $$block13600~d: assert (0 <= $Heap[temp3, C.x]); goto $$block13600~c;
  $$block13600~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp3)) && ($Heap[$p, $ownerFrame] == C)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block13600~b;
  $$block13600~b: $Heap := $Heap[temp3, $inv := C]; goto $$block13600~a;
  $$block13600~a: assume IsHeap($Heap); return;
  
}

procedure System.Object..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(System.Object <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

procedure C..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation C..cctor() {
  entry: goto block14042;
  block14042: goto block14093;
  block14093: return;
  
}

axiom (S <: S);
axiom ($BaseClass(S) == System.Object);
axiom ((S <: $BaseClass(S)) && (AsDirectSubClass(S, $BaseClass(S)) == S));
axiom (!$IsImmutable(S) && ($AsMutable(S) == S));
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: S)} (((IsHeap($h) && ($h[$oi, $inv] <: S)) && ($h[$oi, $localinv] != System.Object)) ==> (((0 <= $h[$oi, S.x]) && (0 <= $h[$oi, S.z])) && (0 <= $h[$oi, S.w]))));
procedure S.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation S.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var stack0i : int;
  var stack1i : int;
  var stack0b : bool;
  var local0 : bool where true;
  var stack50000o : ref;
  var stack0o : ref;
  var SS$Display.Return.Local : bool where true;
  entry: assume $IsNotNull(this, S); goto $$entry~o;
  $$entry~o: assume ($Heap[this, $allocated] == true); goto $$entry~n;
  $$entry~n: throwException := throwException$in; goto block14467;
  block14467: goto block14484;
  block14484: stack0i := 0; goto $$block14484~b;
  $$block14484~b: assert (this != null); goto $$block14484~a;
  $$block14484~a: stack1i := $Heap[this, S.x]; goto true14484to14552, false14484to14501;
  true14484to14552: assume (stack0i > stack1i); goto block14552;
  false14484to14501: assume (stack0i <= stack1i); goto block14501;
  block14552: stack0b := throwException; goto true14552to14603, false14552to14569;
  block14501: stack0i := 0; goto $$block14501~b;
  $$block14501~b: assert (this != null); goto $$block14501~a;
  $$block14501~a: stack1i := $Heap[this, S.z]; goto true14501to14552, false14501to14518;
  true14501to14552: assume (stack0i > stack1i); goto block14552;
  false14501to14518: assume (stack0i <= stack1i); goto block14518;
  block14518: stack0i := 0; goto $$block14518~b;
  $$block14518~b: assert (this != null); goto $$block14518~a;
  $$block14518~a: stack1i := $Heap[this, S.w]; goto true14518to14552, false14518to14535;
  true14552to14603: assume !stack0b; goto block14603;
  false14552to14569: assume stack0b; goto block14569;
  block14603: local0 := false; goto block14654;
  block14569: assume false; goto $$block14569~i;
  $$block14569~i: havoc stack50000o; goto $$block14569~h;
  $$block14569~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block14569~g;
  $$block14569~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block14569~f;
  $$block14569~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block14569~e;
  $$block14569~e: assert (stack50000o != null); goto $$block14569~d;
  $$block14569~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block14569~c;
  $$block14569~c: stack0o := stack50000o; goto $$block14569~b;
  $$block14569~b: assert (stack0o != null); goto $$block14569~a;
  $$block14569~a: assume false; return;
  true14518to14552: assume (stack0i > stack1i); goto block14552;
  false14518to14535: assume (stack0i <= stack1i); goto block14535;
  block14535: goto block14637;
  block14654: SS$Display.Return.Local := local0; goto $$block14654~b;
  $$block14654~b: stack0b := local0; goto $$block14654~a;
  $$block14654~a: $result := stack0b; return;
  block14637: local0 := true; goto block14654;
  
}

procedure S.V0(this : ref);
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == S)) && ($Heap[this, $localinv] == $typeof(this)));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation S.V0(this : ref) {
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : int where InRange(local3, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  entry: assume $IsNotNull(this, S); goto $$entry~p;
  $$entry~p: assume ($Heap[this, $allocated] == true); goto block15538;
  block15538: goto block15691;
  block15691: temp0 := this; goto $$block15691~g;
  $$block15691~g: assert (temp0 != null); goto $$block15691~f;
  $$block15691~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == S)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block15691~e;
  $$block15691~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block15691~d;
  $$block15691~d: havoc temp1; goto $$block15691~c;
  $$block15691~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block15691~b;
  $$block15691~b: assume IsHeap($Heap); goto $$block15691~a;
  $$block15691~a: local2 := null; goto block15708;
  block15708: assert (this != null); goto $$block15708~h;
  $$block15708~h: local3 := $Heap[this, S.x]; goto $$block15708~g;
  $$block15708~g: stack0i := 1; goto $$block15708~f;
  $$block15708~f: stack0i := (local3 + stack0i); goto $$block15708~e;
  $$block15708~e: assert (this != null); goto $$block15708~d;
  $$block15708~d: assert !($Heap[this, $inv] <: S); goto $$block15708~c;
  $$block15708~c: $Heap := $Heap[this, S.x := stack0i]; goto $$block15708~b;
  $$block15708~b: assume IsHeap($Heap); goto $$block15708~a;
  $$block15708~a: stack0i := local3; goto block15793;
  block15793: stack0o := null; goto true15793to15861, false15793to15810;
  true15793to15861: assume (local2 == stack0o); goto block15861;
  false15793to15810: assume (local2 != stack0o); goto block15810;
  block15861: assert (temp0 != null); goto $$block15861~e;
  $$block15861~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block15861~d;
  $$block15861~d: assert (((0 <= $Heap[temp0, S.x]) && (0 <= $Heap[temp0, S.z])) && (0 <= $Heap[temp0, S.w])); goto $$block15861~c;
  $$block15861~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == S)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block15861~b;
  $$block15861~b: $Heap := $Heap[temp0, $inv := S]; goto $$block15861~a;
  $$block15861~a: assume IsHeap($Heap); goto block15844;
  block15810: goto true15810to15861, false15810to15827;
  true15810to15861: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block15861;
  false15810to15827: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block15827;
  block15827: goto block15844;
  block15844: goto block15759;
  block15759: return;
  
}

procedure S.V1(this : ref);
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == S)) && ($Heap[this, $localinv] == $typeof(this)));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation S.V1(this : ref) {
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : int where InRange(local3, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  entry: assume $IsNotNull(this, S); goto $$entry~q;
  $$entry~q: assume ($Heap[this, $allocated] == true); goto block16864;
  block16864: goto block17017;
  block17017: temp0 := this; goto $$block17017~g;
  $$block17017~g: assert (temp0 != null); goto $$block17017~f;
  $$block17017~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == S)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block17017~e;
  $$block17017~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block17017~d;
  $$block17017~d: havoc temp1; goto $$block17017~c;
  $$block17017~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block17017~b;
  $$block17017~b: assume IsHeap($Heap); goto $$block17017~a;
  $$block17017~a: local2 := null; goto block17034;
  block17034: assert (this != null); goto $$block17034~h;
  $$block17034~h: local3 := $Heap[this, S.x]; goto $$block17034~g;
  $$block17034~g: stack0i := 1; goto $$block17034~f;
  $$block17034~f: stack0i := (local3 + stack0i); goto $$block17034~e;
  $$block17034~e: assert (this != null); goto $$block17034~d;
  $$block17034~d: assert !($Heap[this, $inv] <: S); goto $$block17034~c;
  $$block17034~c: $Heap := $Heap[this, S.x := stack0i]; goto $$block17034~b;
  $$block17034~b: assume IsHeap($Heap); goto $$block17034~a;
  $$block17034~a: stack0i := local3; goto block17119;
  block17119: stack0o := null; goto true17119to17187, false17119to17136;
  true17119to17187: assume (local2 == stack0o); goto block17187;
  false17119to17136: assume (local2 != stack0o); goto block17136;
  block17187: assert (temp0 != null); goto $$block17187~e;
  $$block17187~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block17187~d;
  $$block17187~d: assert (((0 <= $Heap[temp0, S.x]) && (0 <= $Heap[temp0, S.z])) && (0 <= $Heap[temp0, S.w])); goto $$block17187~c;
  $$block17187~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == S)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block17187~b;
  $$block17187~b: $Heap := $Heap[temp0, $inv := S]; goto $$block17187~a;
  $$block17187~a: assume IsHeap($Heap); goto block17170;
  block17136: goto true17136to17187, false17136to17153;
  true17136to17187: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block17187;
  false17136to17153: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block17153;
  block17153: goto block17170;
  block17170: goto block17085;
  block17085: return;
  
}

procedure S.V2(this : ref);
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == S)) && ($Heap[this, $localinv] == $typeof(this)));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation S.V2(this : ref) {
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : int where InRange(local3, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, S); goto $$entry~r;
  $$entry~r: assume ($Heap[this, $allocated] == true); goto block18190;
  block18190: goto block18343;
  block18343: temp0 := this; goto $$block18343~j;
  $$block18343~j: havoc stack1s; goto $$block18343~i;
  $$block18343~i: assume $IsTokenForType(stack1s, S); goto $$block18343~h;
  $$block18343~h: stack1o := TypeObject(S); goto $$block18343~g;
  $$block18343~g: assert (temp0 != null); goto $$block18343~f;
  $$block18343~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: S)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block18343~e;
  $$block18343~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block18343~d;
  $$block18343~d: havoc temp1; goto $$block18343~c;
  $$block18343~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block18343~b;
  $$block18343~b: assume IsHeap($Heap); goto $$block18343~a;
  $$block18343~a: local2 := null; goto block18360;
  block18360: assert (this != null); goto $$block18360~h;
  $$block18360~h: local3 := $Heap[this, S.x]; goto $$block18360~g;
  $$block18360~g: stack0i := 1; goto $$block18360~f;
  $$block18360~f: stack0i := (local3 + stack0i); goto $$block18360~e;
  $$block18360~e: assert (this != null); goto $$block18360~d;
  $$block18360~d: assert !($Heap[this, $inv] <: S); goto $$block18360~c;
  $$block18360~c: $Heap := $Heap[this, S.x := stack0i]; goto $$block18360~b;
  $$block18360~b: assume IsHeap($Heap); goto $$block18360~a;
  $$block18360~a: stack0i := local3; goto block18445;
  block18445: stack0o := null; goto true18445to18513, false18445to18462;
  true18445to18513: assume (local2 == stack0o); goto block18513;
  false18445to18462: assume (local2 != stack0o); goto block18462;
  block18513: havoc stack0s; goto $$block18513~h;
  $$block18513~h: assume $IsTokenForType(stack0s, S); goto $$block18513~g;
  $$block18513~g: stack0o := TypeObject(S); goto $$block18513~f;
  $$block18513~f: assert (temp0 != null); goto $$block18513~e;
  $$block18513~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block18513~d;
  $$block18513~d: assert (((0 <= $Heap[temp0, S.x]) && (0 <= $Heap[temp0, S.z])) && (0 <= $Heap[temp0, S.w])); goto $$block18513~c;
  $$block18513~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == S)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block18513~b;
  $$block18513~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block18513~a;
  $$block18513~a: assume IsHeap($Heap); goto block18496;
  block18462: goto true18462to18513, false18462to18479;
  true18462to18513: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block18513;
  false18462to18479: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block18479;
  block18479: goto block18496;
  block18496: goto block18411;
  block18411: return;
  
}

procedure S.V3(this : ref);
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == S)) && ($Heap[this, $localinv] == $typeof(this)));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation S.V3(this : ref) {
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : int where InRange(local3, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, S); goto $$entry~s;
  $$entry~s: assume ($Heap[this, $allocated] == true); goto block19618;
  block19618: goto block19771;
  block19771: temp0 := this; goto $$block19771~j;
  $$block19771~j: havoc stack1s; goto $$block19771~i;
  $$block19771~i: assume $IsTokenForType(stack1s, S); goto $$block19771~h;
  $$block19771~h: stack1o := TypeObject(S); goto $$block19771~g;
  $$block19771~g: assert (temp0 != null); goto $$block19771~f;
  $$block19771~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: S)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block19771~e;
  $$block19771~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block19771~d;
  $$block19771~d: havoc temp1; goto $$block19771~c;
  $$block19771~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block19771~b;
  $$block19771~b: assume IsHeap($Heap); goto $$block19771~a;
  $$block19771~a: local2 := null; goto block19788;
  block19788: assert (this != null); goto $$block19788~h;
  $$block19788~h: local3 := $Heap[this, S.x]; goto $$block19788~g;
  $$block19788~g: stack0i := 1; goto $$block19788~f;
  $$block19788~f: stack0i := (local3 + stack0i); goto $$block19788~e;
  $$block19788~e: assert (this != null); goto $$block19788~d;
  $$block19788~d: assert !($Heap[this, $inv] <: S); goto $$block19788~c;
  $$block19788~c: $Heap := $Heap[this, S.x := stack0i]; goto $$block19788~b;
  $$block19788~b: assume IsHeap($Heap); goto $$block19788~a;
  $$block19788~a: stack0i := local3; goto block19873;
  block19873: stack0o := null; goto true19873to19941, false19873to19890;
  true19873to19941: assume (local2 == stack0o); goto block19941;
  false19873to19890: assume (local2 != stack0o); goto block19890;
  block19941: havoc stack0s; goto $$block19941~h;
  $$block19941~h: assume $IsTokenForType(stack0s, S); goto $$block19941~g;
  $$block19941~g: stack0o := TypeObject(S); goto $$block19941~f;
  $$block19941~f: assert (temp0 != null); goto $$block19941~e;
  $$block19941~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block19941~d;
  $$block19941~d: assert (((0 <= $Heap[temp0, S.x]) && (0 <= $Heap[temp0, S.z])) && (0 <= $Heap[temp0, S.w])); goto $$block19941~c;
  $$block19941~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == S)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block19941~b;
  $$block19941~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block19941~a;
  $$block19941~a: assume IsHeap($Heap); goto block19924;
  block19890: goto true19890to19941, false19890to19907;
  true19890to19941: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block19941;
  false19890to19907: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block19907;
  block19907: goto block19924;
  block19924: goto block19839;
  block19839: return;
  
}

procedure S..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == S)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(S <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation S..ctor(this : ref) {
  var temp0 : ref;
  entry: assume $IsNotNull(this, S); goto $$entry~x;
  $$entry~x: assume ($Heap[this, $allocated] == true); goto $$entry~w;
  $$entry~w: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~v;
  $$entry~v: assume ($Heap[this, S.x] == 0); goto $$entry~u;
  $$entry~u: assume ($Heap[this, S.z] == 0); goto $$entry~t;
  $$entry~t: assume ($Heap[this, S.w] == 0); goto block20791;
  block20791: goto block20808;
  block20808: assert (this != null); goto $$block20808~a;
  $$block20808~a: call System.Object..ctor(this); goto block20876;
  block20876: temp0 := this; goto $$block20876~f;
  $$block20876~f: assert (temp0 != null); goto $$block20876~e;
  $$block20876~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block20876~d;
  $$block20876~d: assert (((0 <= $Heap[temp0, S.x]) && (0 <= $Heap[temp0, S.z])) && (0 <= $Heap[temp0, S.w])); goto $$block20876~c;
  $$block20876~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == S)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block20876~b;
  $$block20876~b: $Heap := $Heap[temp0, $inv := S]; goto $$block20876~a;
  $$block20876~a: assume IsHeap($Heap); return;
  
}

procedure S..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation S..cctor() {
  entry: goto block21165;
  block21165: goto block21216;
  block21216: return;
  
}

axiom (T <: T);
axiom ($BaseClass(T) == S);
axiom ((T <: $BaseClass(T)) && (AsDirectSubClass(T, $BaseClass(T)) == T));
axiom (!$IsImmutable(T) && ($AsMutable(T) == T));
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: T)} (((IsHeap($h) && ($h[$oi, $inv] <: T)) && ($h[$oi, $localinv] != S)) ==> ((0 <= $h[$oi, T.y]) && ($h[$oi, T.y] <= $h[$oi, S.x]))));
procedure T.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation T.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var stack0i : int;
  var stack1i : int;
  var stack0b : bool;
  var local0 : bool where true;
  var stack50000o : ref;
  var stack0o : ref;
  var SS$Display.Return.Local : bool where true;
  entry: assume $IsNotNull(this, T); goto $$entry~z;
  $$entry~z: assume ($Heap[this, $allocated] == true); goto $$entry~y;
  $$entry~y: throwException := throwException$in; goto block21573;
  block21573: goto block21590;
  block21590: stack0i := 0; goto $$block21590~b;
  $$block21590~b: assert (this != null); goto $$block21590~a;
  $$block21590~a: stack1i := $Heap[this, T.y]; goto true21590to21641, false21590to21607;
  true21590to21641: assume (stack0i > stack1i); goto block21641;
  false21590to21607: assume (stack0i <= stack1i); goto block21607;
  block21641: stack0b := throwException; goto true21641to21692, false21641to21658;
  block21607: assert (this != null); goto $$block21607~c;
  $$block21607~c: stack0i := $Heap[this, T.y]; goto $$block21607~b;
  $$block21607~b: assert (this != null); goto $$block21607~a;
  $$block21607~a: stack1i := $Heap[this, S.x]; goto true21607to21641, false21607to21624;
  true21641to21692: assume !stack0b; goto block21692;
  false21641to21658: assume stack0b; goto block21658;
  block21692: local0 := false; goto block21743;
  block21658: assume false; goto $$block21658~i;
  $$block21658~i: havoc stack50000o; goto $$block21658~h;
  $$block21658~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block21658~g;
  $$block21658~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block21658~f;
  $$block21658~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block21658~e;
  $$block21658~e: assert (stack50000o != null); goto $$block21658~d;
  $$block21658~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block21658~c;
  $$block21658~c: stack0o := stack50000o; goto $$block21658~b;
  $$block21658~b: assert (stack0o != null); goto $$block21658~a;
  $$block21658~a: assume false; return;
  true21607to21641: assume (stack0i > stack1i); goto block21641;
  false21607to21624: assume (stack0i <= stack1i); goto block21624;
  block21624: goto block21726;
  block21743: SS$Display.Return.Local := local0; goto $$block21743~b;
  $$block21743~b: stack0b := local0; goto $$block21743~a;
  $$block21743~a: $result := stack0b; return;
  block21726: local0 := true; goto block21743;
  
}

procedure T.V0(this : ref);
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == T)) && ($Heap[this, $localinv] == $typeof(this)));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation T.V0(this : ref) {
  var stack0o : ref;
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local3 : ref where $Is(local3, System.Exception);
  var stack0b : bool;
  entry: assume $IsNotNull(this, T); goto $$entry~aa;
  $$entry~aa: assume ($Heap[this, $allocated] == true); goto block22644;
  block22644: goto block22797;
  block22797: assume (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc)))))); goto block22882;
  block22882: temp0 := this; goto $$block22882~g;
  $$block22882~g: assert (temp0 != null); goto $$block22882~f;
  $$block22882~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == T)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block22882~e;
  $$block22882~e: $Heap := $Heap[temp0, $inv := S]; goto $$block22882~d;
  $$block22882~d: havoc temp1; goto $$block22882~c;
  $$block22882~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block22882~b;
  $$block22882~b: assume IsHeap($Heap); goto $$block22882~a;
  $$block22882~a: local3 := null; goto block22899;
  block22899: assert (this != null); goto $$block22899~a;
  $$block22899~a: call S.V0(this); goto block22984;
  block22984: stack0o := null; goto true22984to23052, false22984to23001;
  true22984to23052: assume (local3 == stack0o); goto block23052;
  false22984to23001: assume (local3 != stack0o); goto block23001;
  block23052: assert (temp0 != null); goto $$block23052~e;
  $$block23052~e: assert (($Heap[temp0, $inv] == S) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block23052~d;
  $$block23052~d: assert ((0 <= $Heap[temp0, T.y]) && ($Heap[temp0, T.y] <= $Heap[temp0, S.x])); goto $$block23052~c;
  $$block23052~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == T)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block23052~b;
  $$block23052~b: $Heap := $Heap[temp0, $inv := T]; goto $$block23052~a;
  $$block23052~a: assume IsHeap($Heap); goto block23035;
  block23001: goto true23001to23052, false23001to23018;
  true23001to23052: assume ($As(local3, Microsoft.Contracts.ICheckedException) != null); goto block23052;
  false23001to23018: assume ($As(local3, Microsoft.Contracts.ICheckedException) == null); goto block23018;
  block23018: goto block23035;
  block23035: goto block22950;
  block22950: return;
  
}

procedure T.V1(this : ref);
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == T)) && ($Heap[this, $localinv] == $typeof(this)));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation T.V1(this : ref) {
  var stack0o : ref;
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local3 : ref where $Is(local3, System.Exception);
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, T); goto $$entry~ab;
  $$entry~ab: assume ($Heap[this, $allocated] == true); goto block24157;
  block24157: goto block24310;
  block24310: assume (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc)))))); goto block24395;
  block24395: temp0 := this; goto $$block24395~j;
  $$block24395~j: havoc stack1s; goto $$block24395~i;
  $$block24395~i: assume $IsTokenForType(stack1s, T); goto $$block24395~h;
  $$block24395~h: stack1o := TypeObject(T); goto $$block24395~g;
  $$block24395~g: assert (temp0 != null); goto $$block24395~f;
  $$block24395~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: T)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block24395~e;
  $$block24395~e: $Heap := $Heap[temp0, $localinv := S]; goto $$block24395~d;
  $$block24395~d: havoc temp1; goto $$block24395~c;
  $$block24395~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block24395~b;
  $$block24395~b: assume IsHeap($Heap); goto $$block24395~a;
  $$block24395~a: local3 := null; goto block24412;
  block24412: assert (this != null); goto $$block24412~a;
  $$block24412~a: call S.V1(this); goto block24497;
  block24497: stack0o := null; goto true24497to24565, false24497to24514;
  true24497to24565: assume (local3 == stack0o); goto block24565;
  false24497to24514: assume (local3 != stack0o); goto block24514;
  block24565: havoc stack0s; goto $$block24565~h;
  $$block24565~h: assume $IsTokenForType(stack0s, T); goto $$block24565~g;
  $$block24565~g: stack0o := TypeObject(T); goto $$block24565~f;
  $$block24565~f: assert (temp0 != null); goto $$block24565~e;
  $$block24565~e: assert ($Heap[temp0, $localinv] == S); goto $$block24565~d;
  $$block24565~d: assert ((0 <= $Heap[temp0, T.y]) && ($Heap[temp0, T.y] <= $Heap[temp0, S.x])); goto $$block24565~c;
  $$block24565~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == T)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block24565~b;
  $$block24565~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block24565~a;
  $$block24565~a: assume IsHeap($Heap); goto block24548;
  block24514: goto true24514to24565, false24514to24531;
  true24514to24565: assume ($As(local3, Microsoft.Contracts.ICheckedException) != null); goto block24565;
  false24514to24531: assume ($As(local3, Microsoft.Contracts.ICheckedException) == null); goto block24531;
  block24531: goto block24548;
  block24548: goto block24463;
  block24463: return;
  
}

procedure T.V2(this : ref);
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == T)) && ($Heap[this, $localinv] == $typeof(this)));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation T.V2(this : ref) {
  var stack0o : ref;
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local3 : ref where $Is(local3, System.Exception);
  var stack0b : bool;
  entry: assume $IsNotNull(this, T); goto $$entry~ac;
  $$entry~ac: assume ($Heap[this, $allocated] == true); goto block25772;
  block25772: goto block25925;
  block25925: assume (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc)))))); goto block26010;
  block26010: temp0 := this; goto $$block26010~g;
  $$block26010~g: assert (temp0 != null); goto $$block26010~f;
  $$block26010~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == T)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block26010~e;
  $$block26010~e: $Heap := $Heap[temp0, $inv := S]; goto $$block26010~d;
  $$block26010~d: havoc temp1; goto $$block26010~c;
  $$block26010~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block26010~b;
  $$block26010~b: assume IsHeap($Heap); goto $$block26010~a;
  $$block26010~a: local3 := null; goto block26027;
  block26027: assert (this != null); goto $$block26027~a;
  $$block26027~a: call S.V2(this); goto block26112;
  block26112: stack0o := null; goto true26112to26180, false26112to26129;
  true26112to26180: assume (local3 == stack0o); goto block26180;
  false26112to26129: assume (local3 != stack0o); goto block26129;
  block26180: assert (temp0 != null); goto $$block26180~e;
  $$block26180~e: assert (($Heap[temp0, $inv] == S) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block26180~d;
  $$block26180~d: assert ((0 <= $Heap[temp0, T.y]) && ($Heap[temp0, T.y] <= $Heap[temp0, S.x])); goto $$block26180~c;
  $$block26180~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == T)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block26180~b;
  $$block26180~b: $Heap := $Heap[temp0, $inv := T]; goto $$block26180~a;
  $$block26180~a: assume IsHeap($Heap); goto block26163;
  block26129: goto true26129to26180, false26129to26146;
  true26129to26180: assume ($As(local3, Microsoft.Contracts.ICheckedException) != null); goto block26180;
  false26129to26146: assume ($As(local3, Microsoft.Contracts.ICheckedException) == null); goto block26146;
  block26146: goto block26163;
  block26163: goto block26078;
  block26078: return;
  
}

procedure T.V3(this : ref);
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == T)) && ($Heap[this, $localinv] == $typeof(this)));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation T.V3(this : ref) {
  var stack0o : ref;
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local3 : ref where $Is(local3, System.Exception);
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, T); goto $$entry~ad;
  $$entry~ad: assume ($Heap[this, $allocated] == true); goto block27285;
  block27285: goto block27438;
  block27438: assume (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc)))))); goto block27523;
  block27523: temp0 := this; goto $$block27523~j;
  $$block27523~j: havoc stack1s; goto $$block27523~i;
  $$block27523~i: assume $IsTokenForType(stack1s, T); goto $$block27523~h;
  $$block27523~h: stack1o := TypeObject(T); goto $$block27523~g;
  $$block27523~g: assert (temp0 != null); goto $$block27523~f;
  $$block27523~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: T)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block27523~e;
  $$block27523~e: $Heap := $Heap[temp0, $localinv := S]; goto $$block27523~d;
  $$block27523~d: havoc temp1; goto $$block27523~c;
  $$block27523~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block27523~b;
  $$block27523~b: assume IsHeap($Heap); goto $$block27523~a;
  $$block27523~a: local3 := null; goto block27540;
  block27540: assert (this != null); goto $$block27540~a;
  $$block27540~a: call S.V3(this); goto block27625;
  block27625: stack0o := null; goto true27625to27693, false27625to27642;
  true27625to27693: assume (local3 == stack0o); goto block27693;
  false27625to27642: assume (local3 != stack0o); goto block27642;
  block27693: havoc stack0s; goto $$block27693~h;
  $$block27693~h: assume $IsTokenForType(stack0s, T); goto $$block27693~g;
  $$block27693~g: stack0o := TypeObject(T); goto $$block27693~f;
  $$block27693~f: assert (temp0 != null); goto $$block27693~e;
  $$block27693~e: assert ($Heap[temp0, $localinv] == S); goto $$block27693~d;
  $$block27693~d: assert ((0 <= $Heap[temp0, T.y]) && ($Heap[temp0, T.y] <= $Heap[temp0, S.x])); goto $$block27693~c;
  $$block27693~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == T)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block27693~b;
  $$block27693~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block27693~a;
  $$block27693~a: assume IsHeap($Heap); goto block27676;
  block27642: goto true27642to27693, false27642to27659;
  true27642to27693: assume ($As(local3, Microsoft.Contracts.ICheckedException) != null); goto block27693;
  false27642to27659: assume ($As(local3, Microsoft.Contracts.ICheckedException) == null); goto block27659;
  block27659: goto block27676;
  block27676: goto block27591;
  block27591: return;
  
}

procedure T.M0(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation T.M0(this : ref) {
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : int where InRange(local3, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, T); goto $$entry~ae;
  $$entry~ae: assume ($Heap[this, $allocated] == true); goto block28815;
  block28815: goto block28968;
  block28968: temp0 := this; goto $$block28968~j;
  $$block28968~j: havoc stack1s; goto $$block28968~i;
  $$block28968~i: assume $IsTokenForType(stack1s, S); goto $$block28968~h;
  $$block28968~h: stack1o := TypeObject(S); goto $$block28968~g;
  $$block28968~g: assert (temp0 != null); goto $$block28968~f;
  $$block28968~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: S)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block28968~e;
  $$block28968~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block28968~d;
  $$block28968~d: havoc temp1; goto $$block28968~c;
  $$block28968~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block28968~b;
  $$block28968~b: assume IsHeap($Heap); goto $$block28968~a;
  $$block28968~a: local2 := null; goto block28985;
  block28985: assert (this != null); goto $$block28985~h;
  $$block28985~h: local3 := $Heap[this, T.y]; goto $$block28985~g;
  $$block28985~g: stack0i := 1; goto $$block28985~f;
  $$block28985~f: stack0i := (local3 + stack0i); goto $$block28985~e;
  $$block28985~e: assert (this != null); goto $$block28985~d;
  $$block28985~d: assert (!($Heap[this, $inv] <: T) || ($Heap[this, $localinv] == S)); goto $$block28985~c;
  $$block28985~c: $Heap := $Heap[this, T.y := stack0i]; goto $$block28985~b;
  $$block28985~b: assume IsHeap($Heap); goto $$block28985~a;
  $$block28985~a: stack0i := local3; goto block29070;
  block29070: stack0o := null; goto true29070to29138, false29070to29087;
  true29070to29138: assume (local2 == stack0o); goto block29138;
  false29070to29087: assume (local2 != stack0o); goto block29087;
  block29138: havoc stack0s; goto $$block29138~h;
  $$block29138~h: assume $IsTokenForType(stack0s, S); goto $$block29138~g;
  $$block29138~g: stack0o := TypeObject(S); goto $$block29138~f;
  $$block29138~f: assert (temp0 != null); goto $$block29138~e;
  $$block29138~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block29138~d;
  $$block29138~d: assert (((0 <= $Heap[temp0, S.x]) && (0 <= $Heap[temp0, S.z])) && (0 <= $Heap[temp0, S.w])); goto $$block29138~c;
  $$block29138~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == S)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block29138~b;
  $$block29138~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block29138~a;
  $$block29138~a: assume IsHeap($Heap); goto block29121;
  block29087: goto true29087to29138, false29087to29104;
  true29087to29138: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block29138;
  false29087to29104: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block29104;
  block29104: goto block29121;
  block29121: goto block29036;
  block29036: return;
  
}

procedure T.M1(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation T.M1(this : ref) {
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : int where InRange(local3, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, T); goto $$entry~af;
  $$entry~af: assume ($Heap[this, $allocated] == true); goto block30243;
  block30243: goto block30396;
  block30396: temp0 := this; goto $$block30396~j;
  $$block30396~j: havoc stack1s; goto $$block30396~i;
  $$block30396~i: assume $IsTokenForType(stack1s, S); goto $$block30396~h;
  $$block30396~h: stack1o := TypeObject(S); goto $$block30396~g;
  $$block30396~g: assert (temp0 != null); goto $$block30396~f;
  $$block30396~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: S)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block30396~e;
  $$block30396~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block30396~d;
  $$block30396~d: havoc temp1; goto $$block30396~c;
  $$block30396~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block30396~b;
  $$block30396~b: assume IsHeap($Heap); goto $$block30396~a;
  $$block30396~a: local2 := null; goto block30413;
  block30413: assert (this != null); goto $$block30413~h;
  $$block30413~h: local3 := $Heap[this, S.x]; goto $$block30413~g;
  $$block30413~g: stack0i := 1; goto $$block30413~f;
  $$block30413~f: stack0i := (local3 + stack0i); goto $$block30413~e;
  $$block30413~e: assert (this != null); goto $$block30413~d;
  $$block30413~d: assert !($Heap[this, $inv] <: S); goto $$block30413~c;
  $$block30413~c: $Heap := $Heap[this, S.x := stack0i]; goto $$block30413~b;
  $$block30413~b: assume IsHeap($Heap); goto $$block30413~a;
  $$block30413~a: stack0i := local3; goto block30498;
  block30498: stack0o := null; goto true30498to30566, false30498to30515;
  true30498to30566: assume (local2 == stack0o); goto block30566;
  false30498to30515: assume (local2 != stack0o); goto block30515;
  block30566: havoc stack0s; goto $$block30566~h;
  $$block30566~h: assume $IsTokenForType(stack0s, S); goto $$block30566~g;
  $$block30566~g: stack0o := TypeObject(S); goto $$block30566~f;
  $$block30566~f: assert (temp0 != null); goto $$block30566~e;
  $$block30566~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block30566~d;
  $$block30566~d: assert (((0 <= $Heap[temp0, S.x]) && (0 <= $Heap[temp0, S.z])) && (0 <= $Heap[temp0, S.w])); goto $$block30566~c;
  $$block30566~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == S)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block30566~b;
  $$block30566~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block30566~a;
  $$block30566~a: assume IsHeap($Heap); goto block30549;
  block30515: goto true30515to30566, false30515to30532;
  true30515to30566: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block30566;
  false30515to30532: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block30532;
  block30532: goto block30549;
  block30549: goto block30464;
  block30464: return;
  
}

procedure T.M2(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation T.M2(this : ref) {
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : int where InRange(local3, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, T); goto $$entry~ag;
  $$entry~ag: assume ($Heap[this, $allocated] == true); goto block31671;
  block31671: goto block31824;
  block31824: temp0 := this; goto $$block31824~j;
  $$block31824~j: havoc stack1s; goto $$block31824~i;
  $$block31824~i: assume $IsTokenForType(stack1s, S); goto $$block31824~h;
  $$block31824~h: stack1o := TypeObject(S); goto $$block31824~g;
  $$block31824~g: assert (temp0 != null); goto $$block31824~f;
  $$block31824~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: S)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block31824~e;
  $$block31824~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block31824~d;
  $$block31824~d: havoc temp1; goto $$block31824~c;
  $$block31824~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block31824~b;
  $$block31824~b: assume IsHeap($Heap); goto $$block31824~a;
  $$block31824~a: local2 := null; goto block31841;
  block31841: assert (this != null); goto $$block31841~h;
  $$block31841~h: local3 := $Heap[this, S.z]; goto $$block31841~g;
  $$block31841~g: stack0i := 1; goto $$block31841~f;
  $$block31841~f: stack0i := (local3 + stack0i); goto $$block31841~e;
  $$block31841~e: assert (this != null); goto $$block31841~d;
  $$block31841~d: assert !($Heap[this, $inv] <: S); goto $$block31841~c;
  $$block31841~c: $Heap := $Heap[this, S.z := stack0i]; goto $$block31841~b;
  $$block31841~b: assume IsHeap($Heap); goto $$block31841~a;
  $$block31841~a: stack0i := local3; goto block31926;
  block31926: stack0o := null; goto true31926to31994, false31926to31943;
  true31926to31994: assume (local2 == stack0o); goto block31994;
  false31926to31943: assume (local2 != stack0o); goto block31943;
  block31994: havoc stack0s; goto $$block31994~h;
  $$block31994~h: assume $IsTokenForType(stack0s, S); goto $$block31994~g;
  $$block31994~g: stack0o := TypeObject(S); goto $$block31994~f;
  $$block31994~f: assert (temp0 != null); goto $$block31994~e;
  $$block31994~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block31994~d;
  $$block31994~d: assert (((0 <= $Heap[temp0, S.x]) && (0 <= $Heap[temp0, S.z])) && (0 <= $Heap[temp0, S.w])); goto $$block31994~c;
  $$block31994~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == S)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block31994~b;
  $$block31994~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block31994~a;
  $$block31994~a: assume IsHeap($Heap); goto block31977;
  block31943: goto true31943to31994, false31943to31960;
  true31943to31994: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block31994;
  false31943to31960: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block31960;
  block31960: goto block31977;
  block31977: goto block31892;
  block31892: return;
  
}

procedure T..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == T)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(T <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation T..ctor(this : ref) {
  var temp0 : ref;
  entry: assume $IsNotNull(this, T); goto $$entry~aj;
  $$entry~aj: assume ($Heap[this, $allocated] == true); goto $$entry~ai;
  $$entry~ai: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~ah;
  $$entry~ah: assume ($Heap[this, T.y] == 0); goto block32844;
  block32844: goto block32861;
  block32861: assert (this != null); goto $$block32861~a;
  $$block32861~a: call S..ctor(this); goto block32929;
  block32929: temp0 := this; goto $$block32929~f;
  $$block32929~f: assert (temp0 != null); goto $$block32929~e;
  $$block32929~e: assert (($Heap[temp0, $inv] == S) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block32929~d;
  $$block32929~d: assert ((0 <= $Heap[temp0, T.y]) && ($Heap[temp0, T.y] <= $Heap[temp0, S.x])); goto $$block32929~c;
  $$block32929~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == T)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block32929~b;
  $$block32929~b: $Heap := $Heap[temp0, $inv := T]; goto $$block32929~a;
  $$block32929~a: assume IsHeap($Heap); return;
  
}

procedure T..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation T..cctor() {
  entry: goto block33218;
  block33218: goto block33269;
  block33269: return;
  
}

axiom (U <: U);
axiom ($BaseClass(U) == T);
axiom ((U <: $BaseClass(U)) && (AsDirectSubClass(U, $BaseClass(U)) == U));
axiom (!$IsImmutable(U) && ($AsMutable(U) == U));
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: U)} (((IsHeap($h) && ($h[$oi, $inv] <: U)) && ($h[$oi, $localinv] != T)) ==> (0 <= $h[$oi, U.u])));
procedure U.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation U.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var stack0i : int;
  var stack1i : int;
  var stack0b : bool;
  var local0 : bool where true;
  var stack50000o : ref;
  var stack0o : ref;
  var SS$Display.Return.Local : bool where true;
  entry: assume $IsNotNull(this, U); goto $$entry~al;
  $$entry~al: assume ($Heap[this, $allocated] == true); goto $$entry~ak;
  $$entry~ak: throwException := throwException$in; goto block33592;
  block33592: goto block33609;
  block33609: stack0i := 0; goto $$block33609~b;
  $$block33609~b: assert (this != null); goto $$block33609~a;
  $$block33609~a: stack1i := $Heap[this, U.u]; goto true33609to33711, false33609to33626;
  true33609to33711: assume (stack0i <= stack1i); goto block33711;
  false33609to33626: assume (stack0i > stack1i); goto block33626;
  block33711: local0 := true; goto block33728;
  block33626: stack0b := throwException; goto true33626to33677, false33626to33643;
  true33626to33677: assume !stack0b; goto block33677;
  false33626to33643: assume stack0b; goto block33643;
  block33677: local0 := false; goto block33728;
  block33643: assume false; goto $$block33643~i;
  $$block33643~i: havoc stack50000o; goto $$block33643~h;
  $$block33643~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block33643~g;
  $$block33643~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block33643~f;
  $$block33643~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block33643~e;
  $$block33643~e: assert (stack50000o != null); goto $$block33643~d;
  $$block33643~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block33643~c;
  $$block33643~c: stack0o := stack50000o; goto $$block33643~b;
  $$block33643~b: assert (stack0o != null); goto $$block33643~a;
  $$block33643~a: assume false; return;
  block33728: SS$Display.Return.Local := local0; goto $$block33728~b;
  $$block33728~b: stack0b := local0; goto $$block33728~a;
  $$block33728~a: $result := stack0b; return;
  
}

procedure U.N0(this : ref);
  requires ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == U)) && ($Heap[this, $localinv] == $typeof(this)));
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation U.N0(this : ref) {
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : int where InRange(local3, System.Int32);
  var stack0i : int;
  var temp2 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp3 : exposeVersionType;
  var local5 : ref where $Is(local5, System.Exception);
  var local6 : int where InRange(local6, System.Int32);
  var local7 : int where InRange(local7, System.Int32);
  var stack0o : ref;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, U); goto $$entry~am;
  $$entry~am: assume ($Heap[this, $allocated] == true); goto block34765;
  block34765: goto block34969;
  block34969: temp0 := this; goto $$block34969~g;
  $$block34969~g: assert (temp0 != null); goto $$block34969~f;
  $$block34969~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == U)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block34969~e;
  $$block34969~e: $Heap := $Heap[temp0, $inv := T]; goto $$block34969~d;
  $$block34969~d: havoc temp1; goto $$block34969~c;
  $$block34969~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block34969~b;
  $$block34969~b: assume IsHeap($Heap); goto $$block34969~a;
  $$block34969~a: local2 := null; goto block34986;
  block34986: assert (this != null); goto $$block34986~s;
  $$block34986~s: local3 := $Heap[this, U.u]; goto $$block34986~r;
  $$block34986~r: stack0i := 1; goto $$block34986~q;
  $$block34986~q: stack0i := (local3 + stack0i); goto $$block34986~p;
  $$block34986~p: assert (this != null); goto $$block34986~o;
  $$block34986~o: assert (!($Heap[this, $inv] <: U) || ($Heap[this, $localinv] == T)); goto $$block34986~n;
  $$block34986~n: $Heap := $Heap[this, U.u := stack0i]; goto $$block34986~m;
  $$block34986~m: assume IsHeap($Heap); goto $$block34986~l;
  $$block34986~l: stack0i := local3; goto $$block34986~k;
  $$block34986~k: temp2 := this; goto $$block34986~j;
  $$block34986~j: havoc stack1s; goto $$block34986~i;
  $$block34986~i: assume $IsTokenForType(stack1s, S); goto $$block34986~h;
  $$block34986~h: stack1o := TypeObject(S); goto $$block34986~g;
  $$block34986~g: assert (temp2 != null); goto $$block34986~f;
  $$block34986~f: assert ((((($Heap[temp2, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp2, $ownerRef], $inv] <: $Heap[temp2, $ownerFrame])) || ($Heap[$Heap[temp2, $ownerRef], $localinv] == $BaseClass($Heap[temp2, $ownerFrame]))) && ($Heap[temp2, $inv] <: S)) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block34986~e;
  $$block34986~e: $Heap := $Heap[temp2, $localinv := System.Object]; goto $$block34986~d;
  $$block34986~d: havoc temp3; goto $$block34986~c;
  $$block34986~c: $Heap := $Heap[temp2, $exposeVersion := temp3]; goto $$block34986~b;
  $$block34986~b: assume IsHeap($Heap); goto $$block34986~a;
  $$block34986~a: local5 := null; goto block35003;
  block35003: assert (this != null); goto $$block35003~q;
  $$block35003~q: local6 := $Heap[this, U.u]; goto $$block35003~p;
  $$block35003~p: stack0i := 1; goto $$block35003~o;
  $$block35003~o: stack0i := (local6 + stack0i); goto $$block35003~n;
  $$block35003~n: assert (this != null); goto $$block35003~m;
  $$block35003~m: assert (!($Heap[this, $inv] <: U) || ($Heap[this, $localinv] == T)); goto $$block35003~l;
  $$block35003~l: $Heap := $Heap[this, U.u := stack0i]; goto $$block35003~k;
  $$block35003~k: assume IsHeap($Heap); goto $$block35003~j;
  $$block35003~j: stack0i := local6; goto $$block35003~i;
  $$block35003~i: assert (this != null); goto $$block35003~h;
  $$block35003~h: local7 := $Heap[this, S.x]; goto $$block35003~g;
  $$block35003~g: stack0i := 1; goto $$block35003~f;
  $$block35003~f: stack0i := (local7 + stack0i); goto $$block35003~e;
  $$block35003~e: assert (this != null); goto $$block35003~d;
  $$block35003~d: assert !($Heap[this, $inv] <: S); goto $$block35003~c;
  $$block35003~c: $Heap := $Heap[this, S.x := stack0i]; goto $$block35003~b;
  $$block35003~b: assume IsHeap($Heap); goto $$block35003~a;
  $$block35003~a: stack0i := local7; goto block35139;
  block35139: stack0o := null; goto true35139to35207, false35139to35156;
  true35139to35207: assume (local5 == stack0o); goto block35207;
  false35139to35156: assume (local5 != stack0o); goto block35156;
  block35207: havoc stack0s; goto $$block35207~h;
  $$block35207~h: assume $IsTokenForType(stack0s, S); goto $$block35207~g;
  $$block35207~g: stack0o := TypeObject(S); goto $$block35207~f;
  $$block35207~f: assert (temp2 != null); goto $$block35207~e;
  $$block35207~e: assert ($Heap[temp2, $localinv] == System.Object); goto $$block35207~d;
  $$block35207~d: assert (((0 <= $Heap[temp2, S.x]) && (0 <= $Heap[temp2, S.z])) && (0 <= $Heap[temp2, S.w])); goto $$block35207~c;
  $$block35207~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp2)) && ($Heap[$p, $ownerFrame] == S)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block35207~b;
  $$block35207~b: $Heap := $Heap[temp2, $localinv := $typeof(temp2)]; goto $$block35207~a;
  $$block35207~a: assume IsHeap($Heap); goto block35190;
  block35156: goto true35156to35207, false35156to35173;
  true35156to35207: assume ($As(local5, Microsoft.Contracts.ICheckedException) != null); goto block35207;
  false35156to35173: assume ($As(local5, Microsoft.Contracts.ICheckedException) == null); goto block35173;
  block35173: goto block35190;
  block35190: goto block35054;
  block35054: goto block35309;
  block35309: stack0o := null; goto true35309to35377, false35309to35326;
  true35309to35377: assume (local2 == stack0o); goto block35377;
  false35309to35326: assume (local2 != stack0o); goto block35326;
  block35377: assert (temp0 != null); goto $$block35377~e;
  $$block35377~e: assert (($Heap[temp0, $inv] == T) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block35377~d;
  $$block35377~d: assert (0 <= $Heap[temp0, U.u]); goto $$block35377~c;
  $$block35377~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == U)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block35377~b;
  $$block35377~b: $Heap := $Heap[temp0, $inv := U]; goto $$block35377~a;
  $$block35377~a: assume IsHeap($Heap); goto block35360;
  block35326: goto true35326to35377, false35326to35343;
  true35326to35377: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block35377;
  false35326to35343: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block35343;
  block35343: goto block35360;
  block35360: goto block35105;
  block35105: return;
  
}

procedure U..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == U)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(U <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation U..ctor(this : ref) {
  var temp0 : ref;
  entry: assume $IsNotNull(this, U); goto $$entry~ap;
  $$entry~ap: assume ($Heap[this, $allocated] == true); goto $$entry~ao;
  $$entry~ao: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~an;
  $$entry~an: assume ($Heap[this, U.u] == 0); goto block36771;
  block36771: goto block36788;
  block36788: assert (this != null); goto $$block36788~a;
  $$block36788~a: call T..ctor(this); goto block36856;
  block36856: temp0 := this; goto $$block36856~f;
  $$block36856~f: assert (temp0 != null); goto $$block36856~e;
  $$block36856~e: assert (($Heap[temp0, $inv] == T) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block36856~d;
  $$block36856~d: assert (0 <= $Heap[temp0, U.u]); goto $$block36856~c;
  $$block36856~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == U)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block36856~b;
  $$block36856~b: $Heap := $Heap[temp0, $inv := U]; goto $$block36856~a;
  $$block36856~a: assume IsHeap($Heap); return;
  
}

procedure U..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation U..cctor() {
  entry: goto block37145;
  block37145: goto block37196;
  block37196: return;
  
}

axiom (D <: D);
axiom ($BaseClass(D) == System.Object);
axiom ((D <: $BaseClass(D)) && (AsDirectSubClass(D, $BaseClass(D)) == D));
axiom (!$IsImmutable(D) && ($AsMutable(D) == D));
procedure D.M0(this : ref);
  requires (((($Heap[$Heap[this, D.t], $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[$Heap[this, D.t], $ownerRef], $inv] <: $Heap[$Heap[this, D.t], $ownerFrame])) || ($Heap[$Heap[$Heap[this, D.t], $ownerRef], $localinv] == $BaseClass($Heap[$Heap[this, D.t], $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[$Heap[this, D.t], $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[$Heap[this, D.t], $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation D.M0(this : ref) {
  var stack0o : ref;
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : ref where $Is(local3, T);
  var local4 : int where InRange(local4, System.Int32);
  var stack0i : int;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, D); goto $$entry~aq;
  $$entry~aq: assume ($Heap[this, $allocated] == true); goto block37723;
  block37723: goto block37876;
  block37876: assert (this != null); goto $$block37876~l;
  $$block37876~l: stack0o := $Heap[this, D.t]; goto $$block37876~k;
  $$block37876~k: temp0 := stack0o; goto $$block37876~j;
  $$block37876~j: havoc stack1s; goto $$block37876~i;
  $$block37876~i: assume $IsTokenForType(stack1s, S); goto $$block37876~h;
  $$block37876~h: stack1o := TypeObject(S); goto $$block37876~g;
  $$block37876~g: assert (temp0 != null); goto $$block37876~f;
  $$block37876~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: S)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block37876~e;
  $$block37876~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block37876~d;
  $$block37876~d: havoc temp1; goto $$block37876~c;
  $$block37876~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block37876~b;
  $$block37876~b: assume IsHeap($Heap); goto $$block37876~a;
  $$block37876~a: local2 := null; goto block37893;
  block37893: assert (this != null); goto $$block37893~j;
  $$block37893~j: local3 := $Heap[this, D.t]; goto $$block37893~i;
  $$block37893~i: assert (local3 != null); goto $$block37893~h;
  $$block37893~h: local4 := $Heap[local3, S.x]; goto $$block37893~g;
  $$block37893~g: stack0i := 1; goto $$block37893~f;
  $$block37893~f: stack0i := (local4 + stack0i); goto $$block37893~e;
  $$block37893~e: assert (local3 != null); goto $$block37893~d;
  $$block37893~d: assert !($Heap[local3, $inv] <: S); goto $$block37893~c;
  $$block37893~c: $Heap := $Heap[local3, S.x := stack0i]; goto $$block37893~b;
  $$block37893~b: assume IsHeap($Heap); goto $$block37893~a;
  $$block37893~a: stack0i := local4; goto block37978;
  block37978: stack0o := null; goto true37978to38046, false37978to37995;
  true37978to38046: assume (local2 == stack0o); goto block38046;
  false37978to37995: assume (local2 != stack0o); goto block37995;
  block38046: havoc stack0s; goto $$block38046~h;
  $$block38046~h: assume $IsTokenForType(stack0s, S); goto $$block38046~g;
  $$block38046~g: stack0o := TypeObject(S); goto $$block38046~f;
  $$block38046~f: assert (temp0 != null); goto $$block38046~e;
  $$block38046~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block38046~d;
  $$block38046~d: assert (((0 <= $Heap[temp0, S.x]) && (0 <= $Heap[temp0, S.z])) && (0 <= $Heap[temp0, S.w])); goto $$block38046~c;
  $$block38046~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == S)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block38046~b;
  $$block38046~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block38046~a;
  $$block38046~a: assume IsHeap($Heap); goto block38029;
  block37995: goto true37995to38046, false37995to38012;
  true37995to38046: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block38046;
  false37995to38012: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block38012;
  block38012: goto block38029;
  block38029: goto block37944;
  block37944: return;
  
}

procedure D.M1(this : ref);
  requires (((($Heap[$Heap[this, D.t], $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[$Heap[this, D.t], $ownerRef], $inv] <: $Heap[$Heap[this, D.t], $ownerFrame])) || ($Heap[$Heap[$Heap[this, D.t], $ownerRef], $localinv] == $BaseClass($Heap[$Heap[this, D.t], $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[$Heap[this, D.t], $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[$Heap[this, D.t], $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation D.M1(this : ref) {
  var stack0o : ref;
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : ref where $Is(local3, T);
  var local4 : int where InRange(local4, System.Int32);
  var stack0i : int;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, D); goto $$entry~ar;
  $$entry~ar: assume ($Heap[this, $allocated] == true); goto block39185;
  block39185: goto block39338;
  block39338: assert (this != null); goto $$block39338~l;
  $$block39338~l: stack0o := $Heap[this, D.t]; goto $$block39338~k;
  $$block39338~k: temp0 := stack0o; goto $$block39338~j;
  $$block39338~j: havoc stack1s; goto $$block39338~i;
  $$block39338~i: assume $IsTokenForType(stack1s, S); goto $$block39338~h;
  $$block39338~h: stack1o := TypeObject(S); goto $$block39338~g;
  $$block39338~g: assert (temp0 != null); goto $$block39338~f;
  $$block39338~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: S)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block39338~e;
  $$block39338~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block39338~d;
  $$block39338~d: havoc temp1; goto $$block39338~c;
  $$block39338~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block39338~b;
  $$block39338~b: assume IsHeap($Heap); goto $$block39338~a;
  $$block39338~a: local2 := null; goto block39355;
  block39355: assert (this != null); goto $$block39355~j;
  $$block39355~j: local3 := $Heap[this, D.t]; goto $$block39355~i;
  $$block39355~i: assert (local3 != null); goto $$block39355~h;
  $$block39355~h: local4 := $Heap[local3, S.w]; goto $$block39355~g;
  $$block39355~g: stack0i := 1; goto $$block39355~f;
  $$block39355~f: stack0i := (local4 + stack0i); goto $$block39355~e;
  $$block39355~e: assert (local3 != null); goto $$block39355~d;
  $$block39355~d: assert !($Heap[local3, $inv] <: S); goto $$block39355~c;
  $$block39355~c: $Heap := $Heap[local3, S.w := stack0i]; goto $$block39355~b;
  $$block39355~b: assume IsHeap($Heap); goto $$block39355~a;
  $$block39355~a: stack0i := local4; goto block39440;
  block39440: stack0o := null; goto true39440to39508, false39440to39457;
  true39440to39508: assume (local2 == stack0o); goto block39508;
  false39440to39457: assume (local2 != stack0o); goto block39457;
  block39508: havoc stack0s; goto $$block39508~h;
  $$block39508~h: assume $IsTokenForType(stack0s, S); goto $$block39508~g;
  $$block39508~g: stack0o := TypeObject(S); goto $$block39508~f;
  $$block39508~f: assert (temp0 != null); goto $$block39508~e;
  $$block39508~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block39508~d;
  $$block39508~d: assert (((0 <= $Heap[temp0, S.x]) && (0 <= $Heap[temp0, S.z])) && (0 <= $Heap[temp0, S.w])); goto $$block39508~c;
  $$block39508~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == S)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block39508~b;
  $$block39508~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block39508~a;
  $$block39508~a: assume IsHeap($Heap); goto block39491;
  block39457: goto true39457to39508, false39457to39474;
  true39457to39508: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block39508;
  false39457to39474: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block39474;
  block39474: goto block39491;
  block39491: goto block39406;
  block39406: return;
  
}

procedure D.M2(this : ref);
  requires ((((($Heap[$Heap[this, D.t], $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[$Heap[this, D.t], $ownerRef], $inv] <: $Heap[$Heap[this, D.t], $ownerFrame])) || ($Heap[$Heap[$Heap[this, D.t], $ownerRef], $localinv] == $BaseClass($Heap[$Heap[this, D.t], $ownerFrame]))) && ($Heap[$Heap[this, D.t], $inv] == T)) && ($Heap[$Heap[this, D.t], $localinv] == $typeof($Heap[this, D.t])));
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation D.M2(this : ref) {
  var stack0o : ref;
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : ref where $Is(local3, T);
  var local4 : int where InRange(local4, System.Int32);
  var stack0i : int;
  var stack0b : bool;
  entry: assume $IsNotNull(this, D); goto $$entry~as;
  $$entry~as: assume ($Heap[this, $allocated] == true); goto block40647;
  block40647: goto block40800;
  block40800: assert (this != null); goto $$block40800~i;
  $$block40800~i: stack0o := $Heap[this, D.t]; goto $$block40800~h;
  $$block40800~h: temp0 := stack0o; goto $$block40800~g;
  $$block40800~g: assert (temp0 != null); goto $$block40800~f;
  $$block40800~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == T)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block40800~e;
  $$block40800~e: $Heap := $Heap[temp0, $inv := S]; goto $$block40800~d;
  $$block40800~d: havoc temp1; goto $$block40800~c;
  $$block40800~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block40800~b;
  $$block40800~b: assume IsHeap($Heap); goto $$block40800~a;
  $$block40800~a: local2 := null; goto block40817;
  block40817: assert (this != null); goto $$block40817~j;
  $$block40817~j: local3 := $Heap[this, D.t]; goto $$block40817~i;
  $$block40817~i: assert (local3 != null); goto $$block40817~h;
  $$block40817~h: local4 := $Heap[local3, S.x]; goto $$block40817~g;
  $$block40817~g: stack0i := 1; goto $$block40817~f;
  $$block40817~f: stack0i := (local4 + stack0i); goto $$block40817~e;
  $$block40817~e: assert (local3 != null); goto $$block40817~d;
  $$block40817~d: assert !($Heap[local3, $inv] <: S); goto $$block40817~c;
  $$block40817~c: $Heap := $Heap[local3, S.x := stack0i]; goto $$block40817~b;
  $$block40817~b: assume IsHeap($Heap); goto $$block40817~a;
  $$block40817~a: stack0i := local4; goto block40902;
  block40902: stack0o := null; goto true40902to40970, false40902to40919;
  true40902to40970: assume (local2 == stack0o); goto block40970;
  false40902to40919: assume (local2 != stack0o); goto block40919;
  block40970: assert (temp0 != null); goto $$block40970~e;
  $$block40970~e: assert (($Heap[temp0, $inv] == S) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block40970~d;
  $$block40970~d: assert ((0 <= $Heap[temp0, T.y]) && ($Heap[temp0, T.y] <= $Heap[temp0, S.x])); goto $$block40970~c;
  $$block40970~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == T)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block40970~b;
  $$block40970~b: $Heap := $Heap[temp0, $inv := T]; goto $$block40970~a;
  $$block40970~a: assume IsHeap($Heap); goto block40953;
  block40919: goto true40919to40970, false40919to40936;
  true40919to40970: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block40970;
  false40919to40936: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block40936;
  block40936: goto block40953;
  block40953: goto block40868;
  block40868: return;
  
}

procedure D..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == D)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(D <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation D..ctor(this : ref) {
  var stack50000o : ref;
  var stack0o : ref;
  var temp0 : exposeVersionType;
  entry: assume $IsNotNull(this, D); goto $$entry~au;
  $$entry~au: assume ($Heap[this, $allocated] == true); goto $$entry~at;
  $$entry~at: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto block41684;
  block41684: goto block41701;
  block41701: havoc stack50000o; goto $$block41701~r;
  $$block41701~r: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == T)); goto $$block41701~q;
  $$block41701~q: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block41701~p;
  $$block41701~p: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block41701~o;
  $$block41701~o: assert (stack50000o != null); goto $$block41701~n;
  $$block41701~n: call T..ctor(stack50000o); goto $$block41701~m;
  $$block41701~m: stack0o := stack50000o; goto $$block41701~l;
  $$block41701~l: assert (this != null); goto $$block41701~k;
  $$block41701~k: havoc temp0; goto $$block41701~j;
  $$block41701~j: $Heap := $Heap[this, $exposeVersion := temp0]; goto $$block41701~i;
  $$block41701~i: $Heap := $Heap[this, D.t := stack0o]; goto $$block41701~h;
  $$block41701~h: assume IsHeap($Heap); goto $$block41701~g;
  $$block41701~g: assert (this != null); goto $$block41701~f;
  $$block41701~f: call System.Object..ctor(this); goto $$block41701~e;
  $$block41701~e: assert (this != null); goto $$block41701~d;
  $$block41701~d: assert (($Heap[this, $inv] == System.Object) && ($Heap[this, $localinv] == $typeof(this))); goto $$block41701~c;
  $$block41701~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == this)) && ($Heap[$p, $ownerFrame] == D)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block41701~b;
  $$block41701~b: $Heap := $Heap[this, $inv := D]; goto $$block41701~a;
  $$block41701~a: assume IsHeap($Heap); return;
  
}

const $stringLiteral0 : ref;
axiom (((forall heap : <x>[ref, name]x :: {heap[$stringLiteral0, $allocated]} (IsHeap(heap) ==> heap[$stringLiteral0, $allocated])) && $IsNotNull($stringLiteral0, System.String)) && ($StringLength($stringLiteral0) == 11));
axiom (((forall heap : <x>[ref, name]x :: {heap[$stringLiteral0, $allocated]} (IsHeap(heap) ==> heap[$stringLiteral0, $allocated])) && $IsNotNull($stringLiteral0, System.String)) && (#System.String.IsInterned$System.String$notnull($stringLiteral0) == $stringLiteral0));
const $stringLiteral1 : ref;
axiom (((forall heap : <x>[ref, name]x :: {heap[$stringLiteral1, $allocated]} (IsHeap(heap) ==> heap[$stringLiteral1, $allocated])) && $IsNotNull($stringLiteral1, System.String)) && ($StringLength($stringLiteral1) == 9));
axiom (((forall heap : <x>[ref, name]x :: {heap[$stringLiteral1, $allocated]} (IsHeap(heap) ==> heap[$stringLiteral1, $allocated])) && $IsNotNull($stringLiteral1, System.String)) && (#System.String.IsInterned$System.String$notnull($stringLiteral1) == $stringLiteral1));
